Prove that some small graphs are acyclic

discouraged

@@ -17267,6 +17267,7 @@ New usage of "poml4N" is discouraged (3 uses).
 New usage of "poml5N" is discouraged (1 uses).
 New usage of "poml6N" is discouraged (1 uses).
 New usage of "prcdnq" is discouraged (14 uses).
+New usage of "prclisacycgr" is discouraged (0 uses).
 New usage of "preleqALT" is discouraged (0 uses).
 New usage of "prlem934" is discouraged (3 uses).
 New usage of "prlem936" is discouraged (1 uses).

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.)  (New usage is discouraged.) $)
+    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.) $)