Prove spthcycl (#3568)

* Prove funen1cnv

* Prove spthcycl

set.mm

@@ -501718,6 +501718,23 @@ have become an indirect lemma of the theorem in question (i.e. a lemma
       YOUVPYLUVOUEYDXQXRYAUVMLYGKGUVNDXHYBTXSXT $.
   $}
 
+  $( A walk is a trivial path if and only if it is both a simple path and a
+     cycle.  (Contributed by BTernaryTau, 8-Oct-2023.) $)
+  spthcycl $p |- ( ( F ( Paths ` G ) P /\ F = (/) ) <->
+      ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) ) $=
+    ( cfv wbr c0 wceq wa wfun cc0 chash co c1 caddc adantr cvv wcel sylan syl
+    wn cpths cspths ccycls ctrls ccnv pthistrl cwlks pthiswlk c1o cen cvtx eqid
+    cfz wlkp ffund wlklenvp1 simp2d hasheq0 biimpar oveq1 0p1e1 syl6eq eqtrd wb
+    simp3d hashen1 biimpa syldan funen1cnv syl2an2r isspth biimpri fveq2 eqcoms
+    wlkv iscycl jca spthispth notnot wne cyclnspth com12 con3dimp sylan2 ancoms
+    nne sylib impbii ) BACUADEZBFGZHZBACUBDEZBACUCDEZHZWKWLWMWIBACUDDEZWJAUEIZW
+    LABCUFWIBACUGDEZWJWPABCUHZWQAIWJAUIUJEZWPWQJBKDZUMLCUKDZAABCXAXAULUNUOWQWJA
+    KDZMGZWSWQWJHZXBWTMNLZMWQXBXEGWJABCUPOXDWTJGZXEMGWQBPQZWJXFWQCPQZXGAPQZABCV
+    OZUQXGXFWJBPURUSRZXFXEJMNLMWTJMNUTVAVBSVCWQXCWSWQXIXCWSVDWQXHXGXIXJVEAPVFSV
+    GVHAVIVJRWLWOWPHABCVKVLVJWIWJJADWTADGZWMWIWQWJXLWRXDXFXLXKXLJWTJWTAVMVNSRWM
+    WIXLHABCVPVLVHVQWNWIWJWLWIWMABCVROWMWLWJWLWMWLTZTZWJWLVSWMXNHBFVTZTWJWMXOXM
+    XOWMXMABCWAWBWCBFWFWGWDWEVQWH $.
+
   $( A non-trivial cycle in a simple graph has a length greater than 2.
      (Contributed by BTernaryTau, 24-Sep-2023.) $)
   usgrgt2cycl $p |- ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) ->