Prove acycgrsubgr (#3605)

* Prove subgrwlk

* Prove subgrtrl

* Prove subgrpth

* Prove subgrcycl

* Rewrap

* Prove acycgrsubgr

Author: BTernaryTau

set.mm

@@ -499245,6 +499245,54 @@ have become an indirect lemma of the theorem in question (i.e. a lemma
       CUQIJVJABCURABCDEUSQSUT $.
   $}
 
+  ${
+    $d P k $.  $d S k $.  $d k F $.  $d k G $.
+    $( If a walk exists in a subgraph of a graph ` G ` , then that walk also
+       exists in ` G ` .  (Contributed by BTernaryTau, 22-Oct-2023.) $)
+    subgrwlk $p |- ( S SubGraph G ->
+          ( F ( Walks ` S ) P -> F ( Walks ` G ) P ) ) $=
+      ( vk wbr cwlks cfv ciedg wcel co wceq wss wral w3a wa cvv eqid syl wi cdm
+      csubgr cword cc0 chash cfz cvtx wf cv c1 caddc csn cpr wif cfzo wb subgrv
+      simpld iswlkg 3simpa cedg cpw subgrprop2 simp2d dmss sswrd 3syl sseld fss
+      simp1d expcom anim12d syl5 3simpb biidd cres subgrprop 3ad2ant1 wrdsymbcl
+      fveq1d fvresd 3adant1 eqtrd eqeq1d sseq2d ifpbi123d biimpd ralrimiv ralim
+      3expia expimpd jcad sylbid df-3an syl6ibr simpl2im sylibrd ) BDUBFZCABGHF
+      ZCDIHZUAZUCZJZUDCUEHZUFKZDUGHZAUHZEUIZAHZXHUJUKKAHZLZXHCHZWTHZXIULZLZXIXJ
+      UMZXMMZUNZEUDXDUOKZNZOZCADGHFZWRWSXCXGPZXTPZYAWRWSCBIHZUAZUCZJZXEBUGHZAUH
+      ZXKXLYEHZXNLZXPYKMZUNZEXSNZOZYDWRBQJZWSYPUPWRYQDQJZBDUQZURAECBYEYIQYIRZYE
+      RZUSSWRYPYCXTYPYHYJPWRYCYHYJYOUTWRYHXCYJXGWRYGXBCWRYEWTMZYFXAMYGXBMWRYIXF
+      MZUUBBVAHZYIVBMZXFWTBUUDDYEYIYTXFRZUUAWTRZUUDRZVCZVDYEWTVEYFXAVFVGVHWRUUC
+      YJXGTWRUUCUUBUUEUUIVJYJUUCXGXEYIXFAVIVKSVLVMYPYHYOPWRXTYHYJYOVNWRYHYOXTWR
+      YHPZYNXRTZEXSNYOXTTUUJUUKEXSWRYHXHXSJZUUKWRYHUULOZYNXRUUMXKYLYMXKXOXQUUMX
+      KVOUUMYKXMXNUUMYKXLWTYFVPZHZXMWRYHYKUUOLUULWRXLYEUUNWRUUCYEUUNLUUEXFWTBUU
+      DDYEYIYTUUFUUAUUGUUHVQVDVTVRYHUULUUOXMLWRYHUULPXLYFWTXHYFCVSWAWBWCZWDUUMY
+      KXMXPUUPWEWFWGWJWHYNXREXSWISWKVMWLWMXCXGXTWNWOWRYQYRYBYAUPYSAECDWTXFQUUFU
+      UGUSWPWQ $.
+  $}
+
+  $( If a trail exists in a subgraph of a graph ` G ` , then that trail also
+     exists in ` G ` .  (Contributed by BTernaryTau, 22-Oct-2023.) $)
+  subgrtrl $p |- ( S SubGraph G ->
+          ( F ( Trails ` S ) P -> F ( Trails ` G ) P ) ) $=
+    ( csubgr wbr cwlks cfv ccnv wfun wa ctrls subgrwlk anim1d istrl 3imtr4g ) B
+    DEFZCABGHFZCIJZKCADGHFZSKCABLHFCADLHFQRTSABCDMNACBOACDOP $.
+
+  $( If a path exists in a subgraph of a graph ` G ` , then that path also
+     exists in ` G ` .  (Contributed by BTernaryTau, 22-Oct-2023.) $)
+  subgrpth $p |- ( S SubGraph G ->
+          ( F ( Paths ` S ) P -> F ( Paths ` G ) P ) ) $=
+    ( csubgr wbr ctrls cfv c1 chash cfzo co cres ccnv wfun cima w3a cpths ispth
+    idd cc0 cpr cin c0 wceq subgrtrl 3anim123d 3imtr4g ) BDEFZCABGHFZAICJHZKLZM
+    NOZAUAUKUBPAULPUCUDUEZQCADGHFZUMUNQCABRHFCADRHFUIUJUOUMUMUNUNABCDUFUIUMTUIU
+    NTUGACBSACDSUH $.
+
+  $( If a cycle exists in a subgraph of a graph ` G ` , then that cycle also
+     exists in ` G ` .  (Contributed by BTernaryTau, 23-Oct-2023.) $)
+  subgrcycl $p |- ( S SubGraph G ->
+          ( F ( Cycles ` S ) P -> F ( Cycles ` G ) P ) ) $=
+    ( csubgr wbr cpths cfv cc0 chash wceq ccycls subgrpth anim1d iscycl 3imtr4g
+    wa ) BDEFZCABGHFZIAHCJHAHKZQCADGHFZTQCABLHFCADLHFRSUATABCDMNACBOACDOP $.
+
   ${
     $d V a b c $.  $d f G p a b c $.
     cusgr3cyclex.1 $e |- V = ( Vtx ` G ) $.
@@ -499602,6 +499650,19 @@ property of an acyclic graph (see also ~ acycgr0v ).  (Contributed by
     NUMUPULURUPULMUMABCORUKUPURMULUKUPURABCPSTUAUSUNUPABCUBUCUHULUQUKABCUDUEUNU
     PUNUFUIUNUGUJ $.
 
+  ${
+    $d S f p $.  $d f G p $.
+    $( The subgraph of an acyclic graph is also acyclic.  (Contributed by
+       BTernaryTau, 23-Oct-2023.) $)
+    acycgrsubgr $p |- ( ( G e. AcyclicGraph /\ S SubGraph G ) ->
+              S e. AcyclicGraph ) $=
+      ( vf vp csubgr wbr cacycgr wcel cv ccycls cfv c0 wne wa wex subgrcycl cvv
+      wn wb isacycgr anim1d 2eximdv con3d subgrv simpl2im simpld 3imtr4d impcom
+      syl ) ABEFZBGHZAGHZUJCIZDIZBJKFZUMLMZNZDOCOZRZUMUNAJKFZUPNZDOCOZRZUKULUJV
+      BURUJVAUQCDUJUTUOUPUNAUMBPUAUBUCUJAQHZBQHZUKUSSABUDZCBQDTUEUJVDULVCSUJVDV
+      EVFUFCAQDTUIUGUH $.
+  $}
+
 $( (End of BTernaryTau's mathbox.) $)