Prove funen1cnv (#3566)

set.mm

@@ -501691,6 +501691,21 @@ have become an indirect lemma of the theorem in question (i.e. a lemma
     wf frn hashss 3adant1 eqbrtrd ) CDFZBEFZABCGZHAIJZCKZIJZBIJZLUEUGUHUJMUFABC
     DNOUFUGUJUKLPZUEUGUFABCTZULABCQUMUFUIBRULABCUABUIEUBSSUCUD $.
 
+  ${
+    $d F p $.  $d x y p $.
+    $( If a function is equinumerous to ordinal 1, then its converse is also a
+       function.  (Contributed by BTernaryTau, 8-Oct-2023.) $)
+    funen1cnv $p |- ( ( Fun F /\ F ~~ 1o ) -> Fun `' F ) $=
+      ( vp vx vy c1o cen wfun ccnv cv csn wceq wex wi wal sylancl syl wa funeqd
+      cnveq biimpar wbr en1 cop wrel wcel funrel vsnid elrel sneq funcnvsn gen2
+      2eximi 19.29r2 exlimivv ax-gen 19.29r funeq imbi12d exlimiv mpan2 impcom
+      sylbi ) AEFUAZAGZAHZGZVCABIZJZKZBLZVDVFMZBAUBVJVHGZVHHZGZMZBNZVKVOBVLVHCI
+      ZDIZUCZJZKZDLCLZVTHZGZDNCNZVNVLVGVSKZDLCLZWBVLVHUDVGVHUEWGVHUFBUGCDVGVHUH
+      OWFWACDVGVSUIULPWDCDVQVRUJUKWBWEQWAWDQZDLCLVNWAWDCDUMWHVNCDWAVNWDWAVMWCVH
+      VTSRTUNPOUOVJVPQVIVOQZBLVKVIVOBUPWIVKBVIVKVOVIVDVLVFVNAVHUQVIVEVMAVHSRURT
+      USPUTVBVA $.
+  $}
+
   $( If a function restricted to a class is one-to-one, then for any two
      elements of the class, the values of the function at those elements are
      equal only if the two elements are the same element.  (Contributed by