From b8bd35fedafb8b0263770b0e15e9b536bc3dd50b Mon Sep 17 00:00:00 2001
From: BTernaryTau <BTernaryTau@users.noreply.github.com>
Date: Mon, 9 Oct 2023 01:01:27 -0400
Subject: [PATCH] Prove funen1cnv (#3566)

---
 set.mm | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/set.mm b/set.mm
index 8eb6a5dda..7a604ce73 100644
--- a/set.mm
+++ b/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