From b98720ec0c244b18e6c12fd19e2859df6aa4311c Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sun, 21 May 2023 23:17:48 +0200
Subject: [PATCH 1/3] edited proof of tz7.48lem

---
 set.mm | 44 ++++++++++++++++++++++----------------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/set.mm b/set.mm
index 25cef3ed7b..88a802e404 100644
--- a/set.mm
+++ b/set.mm
@@ -75873,28 +75873,28 @@ currently used conventions for such cases (see ~ cbvmpt2x , ~ ovmpt2x and
       tz7.48lem $p |- ( ( A C_ On /\ A. x e. A A. y e. x
                     -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` A ) ) $=
         ( vw vz con0 cv cfv wceq wn wral wa weq wi wel wcel wal r2al cres simpl
-        ccnv wfun anim1i imim1i 2alimi sylbi sylibr elequ1 fveq2 eqeq2d imbi12d
-        notbid cbvralv ralbii elequ2 fveqeq2 ralbidv bitri 3bitri ralcom2 ancri
-        wss expd r19.26-2 syl wb fvres eqeqan12d ad2antrl ssel anim12d wo oridm
-        pm3.48 eqcom notbii orbi1i bitr3i syl6ibr con2d word eloni syl2an syl9r
-        ordtri3 biimprd syl6 imp32 exp32 a2d 2alimdv 3imtr4g syl5 imdistani wfn
-        sylbid fnssres mpan cvv wf dffn2 wf1 dff13 df-f1 simprbi sylanb sylan )
-        CHVDZAIZDJZBIZDJZKZLZBXKMACMZNXJXKDCUAZJZXMXRJZKZABOZPZBCMACMZNXRUCUDZX
-        JXQYDXQABQZXNXLKZLZPZBAQZXPPZNZBCMACMZXJYDXQYKBCMZACMZYMXQXKCRZXMCRZNZY
-        KPZBSASZYOXQYPYJNZXPPZBSASYTXPABCXKTUUBYSABUUBYRYJXPYRYJNUUAXPYRYPYJYPY
-        QUBUEUFVEUGUHYKABCCTUIYOYIBCMACMZYONYMYOUUCYOYIACMZBCMZUUCYOFAQZXLFIZDJ
-        ZKZLZPZFCMZACMFGQZGIZDJZUUHKZLZPZFCMZGCMZUUEYNUULACYKUUKBFCBFOZYJUUFXPU
-        UJBFAUJUVAXOUUIUVAXNUUHXLXMUUGDUKULUNUMUOUPUULUUSAGCAGOZUUKUURFCUVBUUFU
-        UMUUJUUQAGFUQUVBUUIUUPXKUUNUUHDURUNUMUSUOUUTAGQZUUOXLKZLZPZACMZGCMUUEUU
-        SUVGGCUURUVFFACFAOZUUMUVCUUQUVEFAGUJUVHUUPUVDUVHUUHXLUUOUUGXKDUKULUNUMU
-        OUPUVGUUDGBCGBOZUVFYIACUVIUVCYFUVEYHGBAUQUVIUVDYGUUNXMXLDURUNUMUSUOUTVA
-        YIBACVBUHVCYIYKABCCVFUIVGXJYRYLPZBSASYRYCPZBSASYMYDXJUVJUVKABXJYRYLYCXJ
-        YRYLYCXJYRYLNNYAXOYBYRYAXOVHXJYLYPYQXSXLXTXNXKCDVIXMCDVIVJVKXJYRYLXOYBP
-        ZXJYRXKHRZXMHRZNZYLUVLPXJYPUVMYQUVNCHXKVLCHXMVLVMYLXOYFYJVNZLZUVOYBYLUV
-        PXOYLUVPYHXPVNZXPYFYHYJXPVPXPXPXPVNUVRXPVOXPYHXPXOYGXLXNVQVRVSVTWAWBUVM
-        XKWCZXMWCZUVQYBPUVNXKWDXMWDUVSUVTNYBUVQXKXMWGWHWEWFWIWJWRWKWLWMYLABCCTY
-        CABCCTWNWOWPXJXRCWQZYDYEDHWQXJUWAEHCDWSWTUWACXAXRXBZYDYECXRXCUWBYDNZUWB
-        YEUWCCXAXRXDUWBYENABCXAXRXECXAXRXFVTXGXHXIVG $.
+        ccnv wfun anim1i imim1i expd 2alimi 3imtr4i eleq1w fveq2 eqeq2d imbi12d
+        notbid cbvralv ralbii elequ2 fveqeq2 ralbidv bitri 3bitri ralcom2 sylbi
+        wss ancri r19.26-2 sylibr syl wb eqeqan12d ad2antrl ssel anim12d pm3.48
+        fvres oridm eqcom notbii orbi1i bitr3i syl6ibr con2d word eloni ordtri3
+        wo biimprd syl2an syl9r syl6 imp32 sylbid a2d 2alimdv 3imtr4g imdistani
+        exp32 syl5 wfn fnssres mpan cvv wf dffn2 wf1 dff13 df-f1 simprbi sylanb
+        sylan ) CHVDZAIZDJZBIZDJZKZLZBXLMACMZNXKXLDCUAZJZXNXSJZKZABOZPZBCMACMZN
+        XSUCUDZXKXRYEXRABQZXOXMKZLZPZBAQZXQPZNZBCMACMZXKYEXRYLBCMZACMZYNXLCRZYK
+        NZXQPZBSASYQXNCRZNZYLPZBSASXRYPYSUUBABYSUUAYKXQUUAYKNYRXQUUAYQYKYQYTUBU
+        EUFUGUHXQABCXLTYLABCCTUIYPYJBCMACMZYPNYNYPUUCYPYJACMZBCMZUUCYPFAQZXMFIZ
+        DJZKZLZPZFCMZACMFGQZGIZDJZUUHKZLZPZFCMZGCMZUUEYOUULACYLUUKBFCBFOZYKUUFX
+        QUUJBFXLUJUVAXPUUIUVAXOUUHXMXNUUGDUKULUNUMUOUPUULUUSAGCAGOZUUKUURFCUVBU
+        UFUUMUUJUUQAGFUQUVBUUIUUPXLUUNUUHDURUNUMUSUOUUTAGQZUUOXMKZLZPZACMZGCMUU
+        EUUSUVGGCUURUVFFACFAOZUUMUVCUUQUVEFAUUNUJUVHUUPUVDUVHUUHXMUUOUUGXLDUKUL
+        UNUMUOUPUVGUUDGBCGBOZUVFYJACUVIUVCYGUVEYIGBAUQUVIUVDYHUUNXNXMDURUNUMUSU
+        OUTVAYJBACVBVCVEYJYLABCCVFVGVHXKUUAYMPZBSASUUAYDPZBSASYNYEXKUVJUVKABXKU
+        UAYMYDXKUUAYMYDXKUUAYMNNYBXPYCUUAYBXPVIXKYMYQYTXTXMYAXOXLCDVOXNCDVOVJVK
+        XKUUAYMXPYCPZXKUUAXLHRZXNHRZNZYMUVLPXKYQUVMYTUVNCHXLVLCHXNVLVMYMXPYGYKW
+        FZLZUVOYCYMUVPXPYMUVPYIXQWFZXQYGYIYKXQVNXQXQXQWFUVRXQVPXQYIXQXPYHXMXOVQ
+        VRVSVTWAWBUVMXLWCZXNWCZUVQYCPUVNXLWDXNWDUVSUVTNYCUVQXLXNWEWGWHWIWJWKWLW
+        QWMWNYMABCCTYDABCCTWOWRWPXKXSCWSZYEYFDHWSXKUWAEHCDWTXAUWACXBXSXCZYEYFCX
+        SXDUWBYENZUWBYFUWCCXBXSXEUWBYFNABCXBXSXFCXBXSXGVTXHXIXJVH $.
     $}
 
     $( Proposition 7.48(2) of [TakeutiZaring] p. 51.  (Contributed by NM,

From afa0c00fd9187b3097d695b2299a32d115cf8a55 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 22 May 2023 00:08:29 +0200
Subject: [PATCH 2/3] added credit

---
 set.mm | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/set.mm b/set.mm
index 88a802e404..9ad4aa6528 100644
--- a/set.mm
+++ b/set.mm
@@ -75869,7 +75869,8 @@ currently used conventions for such cases (see ~ cbvmpt2x , ~ ovmpt2x and
     ${
       $d x A $.
       $( A way of showing an ordinal function is one-to-one.  (Contributed by
-         NM, 9-Feb-1997.) $)
+         NM, 9-Feb-1997.)  Avoid ~ ax-8 .  (Revised by Gino Giotto,
+         22-May-2023.) $)
       tz7.48lem $p |- ( ( A C_ On /\ A. x e. A A. y e. x
                     -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` A ) ) $=
         ( vw vz con0 cv cfv wceq wn wral wa weq wi wel wcel wal r2al cres simpl

From 494f7ac0d0a4d76738158260e9a07b74f698382e Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sat, 12 Aug 2023 08:26:13 +0200
Subject: [PATCH 3/3] removed 'revised by' comment

---
 set.mm | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/set.mm b/set.mm
index 9ad4aa6528..88a802e404 100644
--- a/set.mm
+++ b/set.mm
@@ -75869,8 +75869,7 @@ currently used conventions for such cases (see ~ cbvmpt2x , ~ ovmpt2x and
     ${
       $d x A $.
       $( A way of showing an ordinal function is one-to-one.  (Contributed by
-         NM, 9-Feb-1997.)  Avoid ~ ax-8 .  (Revised by Gino Giotto,
-         22-May-2023.) $)
+         NM, 9-Feb-1997.) $)
       tz7.48lem $p |- ( ( A C_ On /\ A. x e. A A. y e. x
                     -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` A ) ) $=
         ( vw vz con0 cv cfv wceq wn wral wa weq wi wel wcel wal r2al cres simpl