Prove that some small graphs are acyclic

set.mm

@@ -501875,6 +501875,69 @@ it has no (non-trivial) cycles.  (Contributed by BTernaryTau,
       NUOUPUQURUS $.
   $}
 
+  ${
+    $d f g p $.  $d f G p $.  $d f V p $.
+    acycgr0v.1 $e |- V = ( Vtx ` G ) $.
+    $( A null graph (with no vertices) is an acyclic graph.  (Contributed by
+       BTernaryTau, 11-Oct-2023.) $)
+    acycgr0v $p |- ( ( G e. W /\ V = (/) ) -> G e. AcyclicGraph ) $=
+      ( vf vp vg c0 wceq wcel cv ccycls cfv wbr wne wa wex wn df-br nexdv cwlks
+      cacycgr br0 wss cpths cc0 chash cvv df-cycls relmptopab cycliswlk 3imtr3i
+      wb cop relssi cvtx eqeq1i g0wlk0 sylbi syl5sseq breq notbid 3syl intnanrd
+      ss0 mpbiri isacycgr biimpar sylan2 ) BHIZACJZEKZFKZALMZNZVLHOZPZFQZEQRZAU
+      BJZVJVREVJVQFVJVOVPVJVORZVLVMHNZRZVLVMUCVJVNHUDVNHIZWAWCUMVJAUAMZVNHEFVNW
+      EVLVMGKUEMNUFVMMVLUGMVMMIPGEFUHALEGFUIUJVOVLVMWENVLVMUNZVNJWFWEJVMVLAUKVL
+      VMVNSVLVMWESULUOVJAUPMZHIWEHIBWGHDUQAURUSUTVNVEWDVOWBVLVMVNHVAVBVCVFVDTTV
+      KVTVSEACFVGVHVI $.
+  $}
+
+  ${
+    $d f G p $.  $d f V p $.
+    acycgrv.1 $e |- V = ( Vtx ` G ) $.
+    $( A multigraph with one vertex is an acyclic graph.  (Contributed by
+       BTernaryTau, 12-Oct-2023.) $)
+    acycgr1v $p |- ( ( G e. UMGraph /\ ( # ` V ) = 1 ) ->
+              G e. AcyclicGraph ) $=
+      ( vf vp cumgr wcel chash cfv c1 wceq wa cv wbr wal cle wne syl adantr wb
+      cacycgr ccycls c0 wi w3a cc0 clt cpths cyclispth pthhashvtx breq2 3adant1
+      adantl mpbid umgrn1cycl 3adant3 necomd cwlks cycliswlk nn0red 1red ltlend
+      wlkcl 3ad2ant2 mpbir2and cn0 nn0lt10b cvv hasheq0 elv sylib 3com23 3expia
+      3syl alrimivv isacycgr1 mpbird ) AFGZBHIZJKZLZAUAGZDMZEMZAUBINZWCUCKZUDZE
+      ODOZWAWGDEVRVTWEWFVRWEVTWFVRWEVTUEZWCHIZUFKZWFWIWJJUGNZWKWIWLWJJPNZJWJQZW
+      EVTWMVRWEVTLWJVSPNZWMWEWOVTWEWCWDAUHINWOWDWCAUIWDWCABCUJRSVTWOWMTWEVSJWJP
+      UKUMUNULWIWJJVRWEWJJQVTWDWCAUOUPUQWEVRWLWMWNLTZVTWEWCWDAURINZWPWDWCAUSZWQ
+      WJJWQWJWDWCAVCZUTWQVAVBRVDVEWEVRWLWKTZVTWEWQWJVFGWTWRWSWJVGVNVDUNWKWFTDWC
+      VHVIVJVKVLVMVOVRWBWHTVTDAFEVPSVQ $.
+
+    $( A simple graph with two vertices is an acyclic graph.  (Contributed by
+       BTernaryTau, 12-Oct-2023.) $)
+    acycgr2v $p |- ( ( G e. USGraph /\ ( # ` V ) = 2 ) ->
+              G e. AcyclicGraph ) $=
+      ( vf vp cusgr wcel chash cfv c2 wceq wa cv wbr wne wex wn cxr cvv nexdv
+      cacycgr ccycls w3a clt usgrcyclgt2v 2re rexri fvexi hashxrcl ax-mp xrltne
+      c0 cvtx mp3an12 neneqd syl 3expib con2d imp wb isacycgr adantr mpbird ) A
+      FGZBHIZJKZLZAUAGZDMZEMZAUBINZVIULOZLZEPZDPQZVGVNDVGVMEVDVFVMQVDVMVFVDVKVL
+      VFQZVDVKVLUCJVEUDNZVPVJVIABCUEVQVEJJRGVERGZVQVEJOJUFUGBSGVRBAUMCUHBSUIUJJ
+      VEUKUNUOUPUQURUSTTVDVHVOUTVFDAFEVAVBVC $.
+  $}
+
+  ${
+    $d f g p $.  $d f G p $.  $d f V p $.
+    prclisacycgr.1 $e |- V = ( Vtx ` G ) $.
+    $( A proper class (representing a null graph, see ~ vtxvalprc ) has the
+       property of an acyclic graph (see also ~ acycgr0v ).  (Contributed by
+       BTernaryTau, 11-Oct-2023.) $)
+    prclisacycgr $p |- ( -. G e. _V ->
+              -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) $=
+      ( vg cvv wcel wn c0 wceq cv ccycls cfv wbr wa wex cvtx df-br nexdv syl5eq
+      wne fvprc br0 wss cwlks cpths cc0 chash df-cycls relmptopab cop cycliswlk
+      3imtr3i relssi eqeq1i g0wlk0 sylbi syl5sseq ss0 breq notbid 3syl intnanrd
+      wb mpbiri syl ) BGHIZCJKZALZDLZBMNZOZVJJUBZPZDQZAQIVHCBRNZJEBRUCUAVIVPAVI
+      VODVIVMVNVIVMIZVJVKJOZIZVJVKUDVIVLJUEVLJKZVRVTVEVIBUFNZVLJADVLWBVJVKFLUGN
+      OUHVKNVJUINVKNKPFADGBMAFDUJUKVMVJVKWBOVJVKULZVLHWCWBHVKVJBUMVJVKVLSVJVKWB
+      SUNUOVIVQJKWBJKCVQJEUPBUQURUSVLUTWAVMVSVJVKVLJVAVBVCVFVDTTVG $.
+  $}
+
 $( (End of BTernaryTau's mathbox.) $)