Prove tz7.48lem without ax-8

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,