metamath · avekens · Oct 11, 2024 · Oct 7, 2024
diff --git a/set.mm b/set.mm
@@ -62378,14 +62378,31 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
     UMSZUOAUNULHZVACTZAUPUAZSZVBUKVEUMUKVCVDABCUBUKUQVDURAUPUCNUDUEACUFNUMUOVBU
     GUKAUNCULUHUIUJQ $.
 
-  $( Composition of onto functions.  (Contributed by NM, 22-Mar-2006.) $)
+  $( The preimage of the codomain of a surjection is its domain.  (Contributed
+     by AV, 29-Sep-2024.) $)
+  focnvimacdmdm $p |- ( G : A -onto-> B -> ( `' G " B ) = A ) $=
+    ( wfo ccnv cima cdm crn forn eqcomd imaeq2d cnvimarndm eqtrdi fdmd eqtrd
+    fof ) ABCDZCEZBFZCGZAQSRCHZFTQBUARQUABABCIJKCLMQABCABCPNO $.
+
+  $( Composition of onto functions.  Generalisation of ~ foco .  (Contributed
+     by AV, 29-Sep-2024.) $)
+  focofo $p |- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G )
+                 -> ( F o. G ) : ( `' G " A ) -onto-> B ) $=
+    ( wfo wfun crn wss w3a ccnv cima ccom wceq fcof sylan 3adant3 cres 3ad2ant1
+    wf fof rnco cdm freld fdm eqcomd syl sseq1d biimpa relssres rneqd 3imp3i2an
+    wrel wa forn eqtrd syl5eq dffo2 sylanbrc ) ABCEZDFZADGZHZIZDJAKZBCDLZSZVEGZ
+    BMVDBVEEUSUTVFVBUSABCSZUTVFABCTZABCDNOPVCVGCVAQZGZBCDUAVCVKCGZBUSUTVBCULZCU
+    BZVAHZVKVLMUSUTVMVBUSABCVIUCRUSVBVOUSAVNVAUSVHAVNMVIVHVNAABCUDUEUFUGUHVMVOU
+    MVJCCVAUIUJUKUSUTVLBMVBABCUNRUOUPVDBVEUQUR $.
+
+  $( Composition of onto functions.  (Contributed by NM, 22-Mar-2006.)  (Proof
+     shortened by AV, 29-Sep-2024.) $)
   foco $p |- ( ( F : B -onto-> C /\ G : A -onto-> B ) ->
              ( F o. G ) : A -onto-> C ) $=
-    ( wfo wa ccom crn wceq dffo2 fco ad2ant2r cdm fdm eqtr3 sylan rncoeq eqeq1d
-    wf biimpar an32s adantrl jca syl2anb sylibr ) BCDFZABEFZGACDEHZTZUIIZCJZGZA
-    CUIFUGBCDTZDIZCJZGZABETZEIZBJZGZUMUHBCDKABEKUQVAGUJULUNURUJUPUTABCDELMUQUTU
-    LURUNUTUPULUNUTGDNZUSJZUPULUNVBBJUTVCBCDOVBUSBPQVCULUPVCUKUOCDERSUAQUBUCUDU
-    EACUIKUF $.
+    ( wfo ccom ccnv cima wfun crn wss simpl fofun adantl wceq forn eqimss2 syl
+    wa focofo syl3anc wb focnvimacdmdm eqcomd foeq2 mpbird ) BCDFZABEFZTZACDEGZ
+    FZEHBIZCUKFZUJUHEJZBEKZLZUNUHUIMUIUOUHABENOUIUQUHUIUPBPUQABEQBUPRSOBCDEUAUB
+    UJAUMPZULUNUCUIURUHUIUMAABEUDUEOAUMCUKUFSUG $.
 
   $( A nonzero constant function is onto.  (Contributed by NM, 12-Jan-2007.) $)
   foconst $p |- ( ( F : A --> { B } /\ F =/= (/) ) -> F : A -onto-> { B } ) $=
@@ -64844,17 +64861,17 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
 
   ${
     rescnvimafod.f $e |- ( ph -> F Fn A ) $.
-    rescnvimafod.e $e |- E = ( ran F i^i B ) $.
-    rescnvimafod.d $e |- D = ( `' F " B ) $.
+    rescnvimafod.e $e |- ( ph -> E = ( ran F i^i B ) ) $.
+    rescnvimafod.d $e |- ( ph -> D = ( `' F " B ) ) $.
     $( The restriction of a function to a preimage of a class is a function
        onto the intersection of this class and the range of the function.
-       (Contributed by AV, 13-Sep-2024.) $)
+       (Contributed by AV, 13-Sep-2024.)  (Revised by AV, 29-Sep-2024.) $)
     rescnvimafod $p |- ( ph -> ( F |` D ) : D -onto-> E ) $=
       ( cres wfn crn wceq wfo ccnv cima cdm wss a1i cin cnvimass eqcomd 3sstr4d
-      fndmd fnssresd imaeq2i fnfun funimacnv incom 3eqtrd df-ima eqcomi 3eqtr4g
-      wfun 3syl df-fo sylanbrc ) AFDJZDKURLZEMDEURNABDFGAFOCPZFQZDBUTVARAFCUASD
-      UTMAISAVABABFGUDUBUCUEAFDPZFLZCTZUSEAVBFUTPZCVCTZVDVBVEMADUTFIUFSAFBKFUNV
-      EVFMGBFUGCFUHUOVFVDMACVCUISUJVBUSFDUKULHUMDEURUPUQ $.
+      fndmd fnssresd df-ima imaeq2d fnfun funimacnv incom 3eqtrd eqtr3id eqtr4d
+      wfun 3syl df-fo sylanbrc ) AFDJZDKURLZEMDEURNABDFGAFOCPZFQZDBUTVARAFCUASI
+      AVABABFGUDUBUCUEAUSFLZCTZEAUSFDPZVCFDUFAVDFUTPZCVBTZVCADUTFIUGAFBKFUNVEVF
+      MGBFUHCFUIUOVFVCMACVBUJSUKULHUMDEURUPUQ $.
   $}
 
   ${
@@ -749582,6 +749599,14 @@ but which is a consequence of that a contradiction implies anything (see
       UOURUOUPUHUIUJABDEUKTVAAULUMUN $.
   $}
 
+  $( Conditions for a restriction to be an onto function.  Part of ~ fresf1o .
+     (Contributed by AV, 29-Sep-2024.) $)
+  fresfo $p |- ( ( Fun F /\ C C_ ran F )
+                 -> ( F |` ( `' F " C ) ) : ( `' F " C ) -onto-> C ) $=
+    ( wfun crn wss wa cdm ccnv cima wfn funfn biimpi adantr wceq sseqin2 eqcomd
+    cin adantl eqidd rescnvimafod ) BCZABDZEZFZBGZABHAIZABUABUEJZUCUAUGBKLMUCAU
+    BAQZNUAUCUHAUCUHANAUBOLPRUDUFST $.
+
   ${
     $d B b f g $.  $d S b f g $.  $d V b g $.
     $( The class of all functions from a (proper) singleton into ` B ` is the
@@ -749795,8 +749820,9 @@ class of all the singletons of (proper) ordered pairs over the elements
 
     $( Lemma 3 for ~ fcores .  (Contributed by AV, 13-Sep-2024.) $)
     fcoreslem3 $p |- ( ph -> X : P -onto-> E ) $=
-      ( wfo cres ffnd rescnvimafod wceq wb foeq1 mp1i mpbird ) AEFHMZEFGENZMZAB
-      DEFGABCGIOJKPHUCQUBUDRALEFHUCSTUA $.
+      ( wfo cres ffnd crn cin wceq a1i ccnv cima rescnvimafod foeq1 mp1i mpbird
+      wb ) AEFHMZEFGENZMZABDEFGABCGIOFGPDQRAJSEGTDUARAKSUBHUHRUGUIUFALEFHUHUCUD
+      UE $.
 
     fcores.g $e |- ( ph -> G : C --> D ) $.
     fcores.y $e |- Y = ( G |` E ) $.
@@ -749839,35 +749865,44 @@ restrictions of the composed functions (to their minimum domains).
       fcoresf1.i $e |- ( ph -> ( G o. F ) : P -1-1-> D ) $.
       $( If a composition is injective, then the restrictions of its components
          to the minimum domains are injective.  (Contributed by GL and AV,
-         18-Sep-2024.) $)
-      fcoresf1 $p |- ( ph -> ( X : P -1-1-onto-> E /\ Y : E -1-1-> D ) ) $=
-        ( wceq wi vx vy va vb wf1o wf1 wfo wf cv cfv wral fcoreslem3 fof syl wa
-        ccom dff13 wcel fcoresf1lem adantrr adantrl eqeq12d imbi1d fveq2 imim1d
-        a1i sylbid ralimdvva adantld syl5bi sylanbrc df-f1o cres inss2 eqsstrdi
-        mpd crn cin fssresd feq1i sylibr wrex fcoreslem2 eqcomd eleq2d wfn fofn
-        fvelrnb bitrd anbi12d fveqeq2 eqeq1 imbi12d eqeq2d rspc2v adantl imim2d
-        wb equequ2 syld com23 impl eqeqan12rd eqeq12 ancoms syl5ibcom rexlimdva
-        ex expd impd ralrimivv jca ) AFGJUEZGEKUFZAFGJUFZFGJUGZXMAFGJUHZUAUIZJU
-        JZUBUIZJUJZSZXRXTSZTZUBFUKUAFUKZXOAXPXQABCDFGHJLMNOULZFGJUMUNAFEIHUPZUF
-        ZYERYHFEYGUHZXRYGUJZXTYGUJZSZYCTZUBFUKUAFUKZUOZAYEUAUBFEYGUQZAYNYEYIAYM
-        YDUAUBFFAXRFURZXTFURZUOUOZYMXSKUJZYAKUJZSZYCTYDYSYLUUBYCYSYJYTYKUUAAYQY
-        JYTSYRABCDEFGHIJKXRLMNOPQUSUTAYRYKUUASYQABCDEFGHIJKXTLMNOPQUSVAVBVCYSYB
-        UUBYCYBUUBTYSXSYAKVDVFVEVGVHVIVJVPUAUBFGJUQVKYFFGJVLVKAGEKUHZXRKUJZXTKU
-        JZSZYCTZUBGUKUAGUKXNAGEIGVMZUHUUCADEGIPAGHVQZDVRZDGUUJSAMVFUUIDVNVOVSGE
-        KUUHQVTWAAUUGUAUBGGAXRGURZXTGURZUOUCUIZJUJZXRSZUCFWBZUDUIZJUJZXTSZUDFWB
-        ZUOUUGAUUKUUPUULUUTAUUKXRJVQZURZUUPAGUVAXRAUVAGABCDFGHJLMNOWCWDZWEAJFWF
-        ZUVBUUPWRAXPUVDYFFGJWGUNZUCFXRJWHUNWIAUULXTUVAURZUUTAGUVAXTUVCWEAUVDUVF
-        UUTWRUVEUDFXTJWHUNWIWJAUUPUUTUUGAUUOUUTUUGTUCFAUUMFURZUOZUUTUUOUUGUVHUU
-        SUUOUUGTUDFUVHUUQFURZUOZUUSUUOUUGUVJUUNKUJZUURKUJZSZUUNUURSZTZUUSUUOUOZ
-        UUGAUVGUVIUVOAYHUVGUVIUOZUVOTZRYHYOAUVRYPAYNUVRYIAUVQYNUVOAUVQYNUVOTAUV
-        QUOZYNUUMYGUJZUUQYGUJZSZUUMUUQSZTZUVOUVQYNUWDTAYMUWDUVTYKSZUUMXTSZTUAUB
-        UUMUUQFFXRUUMSYLUWEYCUWFXRUUMYKYGWKXRUUMXTWLWMXTUUQSZUWEUWBUWFUWCUWGYKU
-        WAUVTXTUUQYGVDWNUBUDUCWSWMWOWPUVSUWDUVMUWCTUVOUVSUWBUVMUWCUVSUVTUVKUWAU
-        VLAUVGUVTUVKSUVIABCDEFGHIJKUUMLMNOPQUSUTAUVIUWAUVLSUVGABCDEFGHIJKUUQLMN
-        OPQUSVAVBVCUVSUWCUVNUVMUWCUVNTUVSUUMUUQJVDVFWQVGWTXHXAVIVJVPXBUVPUVMUUF
-        UVNYCUUOUUSUVKUUDUVLUUEUUNXRKVDUURXTKVDXCUUOUUSUVNYCWRUUNXRUURXTXDXEWMX
-        FXIXGXAXGXJVGXKUAUBGEKUQVKXL $.
-    $}
+         18-Sep-2024.)  (Revised by AV, 7-Oct-2024.) $)
+      fcoresf1 $p |- ( ph -> ( X : P -1-1-> E /\ Y : E -1-1-> D ) ) $=
+        ( wceq wi vx vy va vb wf1 wf cv cfv wral wfo fcoreslem3 fof syl ccom wa
+        dff13 wcel fcoresf1lem adantrr adantrl eqeq12d imbi1d a1i imim1d sylbid
+        fveq2 ralimdvva adantld syl5bi mpd sylanbrc cres crn cin inss2 eqsstrdi
+        fssresd feq1i sylibr wrex fcoreslem2 eqcomd eleq2d wfn wb fvelrnb bitrd
+        fofn anbi12d fveqeq2 eqeq1 imbi12d eqeq2d equequ2 rspc2v adantl syld ex
+        imim2d impl eqeqan12rd eqeq12 ancoms syl5ibcom expd rexlimdva ralrimivv
+        com23 impd jca ) AFGJUEZGEKUEZAFGJUFZUAUGZJUHZUBUGZJUHZSZXNXPSZTZUBFUIU
+        AFUIZXKAFGJUJZXMABCDFGHJLMNOUKZFGJULUMAFEIHUNZUEZYARYEFEYDUFZXNYDUHZXPY
+        DUHZSZXSTZUBFUIUAFUIZUOZAYAUAUBFEYDUPZAYKYAYFAYJXTUAUBFFAXNFUQZXPFUQZUO
+        UOZYJXOKUHZXQKUHZSZXSTXTYPYIYSXSYPYGYQYHYRAYNYGYQSYOABCDEFGHIJKXNLMNOPQ
+        URUSAYOYHYRSYNABCDEFGHIJKXPLMNOPQURUTVAVBYPXRYSXSXRYSTYPXOXQKVFVCVDVEVG
+        VHVIVJUAUBFGJUPVKAGEKUFZXNKUHZXPKUHZSZXSTZUBGUIUAGUIXLAGEIGVLZUFYTADEGI
+        PAGHVMZDVNZDGUUGSAMVCUUFDVOVPVQGEKUUEQVRVSAUUDUAUBGGAXNGUQZXPGUQZUOUCUG
+        ZJUHZXNSZUCFVTZUDUGZJUHZXPSZUDFVTZUOUUDAUUHUUMUUIUUQAUUHXNJVMZUQZUUMAGU
+        URXNAUURGABCDFGHJLMNOWAWBZWCAJFWDZUUSUUMWEAYBUVAYCFGJWHUMZUCFXNJWFUMWGA
+        UUIXPUURUQZUUQAGUURXPUUTWCAUVAUVCUUQWEUVBUDFXPJWFUMWGWIAUUMUUQUUDAUULUU
+        QUUDTUCFAUUJFUQZUOZUUQUULUUDUVEUUPUULUUDTUDFUVEUUNFUQZUOZUUPUULUUDUVGUU
+        KKUHZUUOKUHZSZUUKUUOSZTZUUPUULUOZUUDAUVDUVFUVLAYEUVDUVFUOZUVLTZRYEYLAUV
+        OYMAYKUVOYFAUVNYKUVLAUVNYKUVLTAUVNUOZYKUUJYDUHZUUNYDUHZSZUUJUUNSZTZUVLU
+        VNYKUWATAYJUWAUVQYHSZUUJXPSZTUAUBUUJUUNFFXNUUJSYIUWBXSUWCXNUUJYHYDWJXNU
+        UJXPWKWLXPUUNSZUWBUVSUWCUVTUWDYHUVRUVQXPUUNYDVFWMUBUDUCWNWLWOWPUVPUWAUV
+        JUVTTUVLUVPUVSUVJUVTUVPUVQUVHUVRUVIAUVDUVQUVHSUVFABCDEFGHIJKUUJLMNOPQUR
+        USAUVFUVRUVISUVDABCDEFGHIJKUUNLMNOPQURUTVAVBUVPUVTUVKUVJUVTUVKTUVPUUJUU
+        NJVFVCWSVEWQWRXHVHVIVJWTUVMUVJUUCUVKXSUULUUPUVHUUAUVIUUBUUKXNKVFUUOXPKV
+        FXAUULUUPUVKXSWEUUKXNUUOXPXBXCWLXDXEXFXHXFXIVEXGUAUBGEKUPVKXJ $.
+    $}
+
+    $( A composition is injective iff the restrictions of its components to the
+       minimum domains are injective.  (Contributed by GL and AV,
+       7-Oct-2024.) $)
+    fcoresf1b $p |- ( ph -> ( ( G o. F ) : P -1-1-> D
+                              <-> ( X : P -1-1-> E /\ Y : E -1-1-> D ) ) ) $=
+      ( ccom wf1 wa wf adantr simpr fcoresf1 ex f1co ancoms wb fcores f1eq1 syl
+      wceq syl5ibr impbid ) AFEIHRZSZFGJSZGEKSZTZAUPUSAUPTBCDEFGHIJKABCHUAUPLUB
+      MNOADEIUAUPPUBQAUPUCUDUEUSUPAFEKJRZSZURUQVAFGEKJUFUGAUOUTULUPVAUHABCDEFGH
+      IJKLMNOPQUIFEUOUTUJUKUMUN $.
 
     ${
       fcoresfo.s $e |- ( ph -> ( G o. F ) : P -onto-> D ) $.
@@ -749882,6 +749917,27 @@ restrictions of the composed functions (to their minimum domains).
         JKLMNOPQUPUQFEVDVIURUNUSFGEKJUTVA $.
     $}
 
+    $( A composition is surjective iff the restriction of its first component
+       to the minimum domain is surjective.  (Contributed by GL and AV,
+       7-Oct-2024.) $)
+    fcoresfob $p |- ( ph -> ( ( G o. F ) : P -onto-> D
+                              <-> Y : E -onto-> D ) ) $=
+      ( wfo wa adantr ccom wf simpr fcoresfo fcoreslem3 anim1ci foco syl fcores
+      wceq wb foeq1 mpbird impbida ) AFEIHUAZRZGEKRZAUPSBCDEFGHIJKABCHUBUPLTMNO
+      ADEIUBUPPTQAUPUCUDAUQSZUPFEKJUAZRZURUQFGJRZSUTAVAUQABCDFGHJLMNOUEUFFGEKJU
+      GUHURUOUSUJZUPUTUKAVBUQABCDEFGHIJKLMNOPQUITFEUOUSULUHUMUN $.
+
+    $( A composition is bijective iff the restriction of its first component to
+       the minimum domain is bijective and the restriction of its second
+       component to the minimum domain is injective.  (Contributed by GL and
+       AV, 7-Oct-2024.) $)
+    fcoresf1ob $p |- ( ph -> ( ( G o. F ) : P -1-1-onto-> D
+                           <-> ( X : P -1-1-> E /\ Y : E -1-1-onto-> D ) ) ) $=
+      ( wf1 wfo wa ccom fcoresf1b fcoresfob anbi12d anass bitrdi df-f1o 3bitr4g
+      wf1o anbi2i ) AFEIHUAZRZFEUKSZTZFGJRZGEKRZGEKSZTZTZFEUKUIUOGEKUIZTAUNUOUP
+      TZUQTUSAULVAUMUQABCDEFGHIJKLMNOPQUBABCDEFGHIJKLMNOPQUCUDUOUPUQUEUFFEUKUGU
+      TURUOGEKUGUJUH $.
+
     ${
       f1cof1blem.s $e |- ( ph -> ran F = C ) $.
       $( Lemma for ~ f1cof1b and ~ focofob .  (Contributed by AV,
@@ -749904,52 +749960,85 @@ restrictions of the composed functions (to their minimum domains).
   f1cof1b $p |- ( ( F : A --> B /\ G : C --> D /\ ran F = C )
                   -> ( ( G o. F ) : A -1-1-> D
                        <-> ( F : A -1-1-> B /\ G : C -1-1-> D ) ) ) $=
-    ( wf wceq wf1 wa cima cres eqid simpll adantr simpr ancomd f1eq123d syl5ib
-    wb crn w3a ccom ccnv cin simp1 simp2 simp3 f1cof1blem f1eq2 3syl wf1o ancom
-    bicomd anbi2i sylibr fcoresf1 simprl eqidd biimpd f1of1 simprr anim12d sylc
-    sylbida wfun ffrn ax-1 impbid2 anbi1d df-f1 3bitr4g 3ad2ant1 f1eq3 3ad2ant3
-    bitrd anbi2d mpbird f1cof1 ancoms cdm imaeq2 cnvimarndm eqtrdi eqcoms eqtrd
-    ex fdmd syl impbid ) ABEGZCDFGZEUAZCHZUBZADFEUCZIZABEIZCDFIZJZWOWQWTWOWQJZW
-    SWRXAWSWRJZWSACEIZJZWOWQEUDZCKZDWPIZXDWOXGWQWOXFAHZWMCUEZCHZJZEXFLZEHZFXILZ
-    FHZJZJZXHXGWQTZWOABCDXFXIEFXLXNWKWLWNUFZXIMZXFMZXLMZWKWLWNUGZXNMZWKWLWNUHUI
-    ZXHXJXPNXFADWPUJZUKUNWOXGJZXKXOXMJZJZXIDXNIZXFXIXLULZJXDWOYIXGWOXQYIYEYHXPX
-    KXOXMUMUOUPOYGYKYJYGABCDXFXIEFXLXNWOWKXGXSOXTYAYBWOWLXGYCOYDWOXGPUQQYIYJWSY
-    KXCYIYJWSYIXICDDXNFXKXOXMURXKXJYHXHXJPOZYIDUSRUTYKXFXIXLIYIXCXFXIXLVAYIXFAX
-    ICXLEXKXOXMVBXHXJYHNYLRSVCVDVEWOXBXDTWQWOWRXCWSWOWRAWMEIZXCWKWLWRYMTWNWKWKX
-    EVFZJAWMEGZYNJWRYMWKWKYOYNWKWKYOABEVGWKYOVHVIVJABEVKAWMEVKVLVMWNWKYMXCTWLWM
-    CAEVNVOVPVQOVRQWGWTXGWOWQWSWRXGABCDFEVSVTWOXHXRWOXFEWAZAWNWKXFYPHZWLYQCWMCW
-    MHXFXEWMKYPCWMXEWBEWCWDWEVOWOABEXSWHWFYFWISWJ $.
-
-  $( If the range of ` F ` equals the domain of ` G ` , then the composition
-     ` ( G o. F ) ` is surjective iff ` F ` and ` G ` are both surjective .
-     (Contributed by GL and AV, 20-Sep-2024.) $)
+    ( wf wceq wf1 wa cima cres eqid simpll adantr simpr ancomd f1eq123d biimpd
+    wb crn w3a ccom ccnv simp1 simp2 simp3 f1cof1blem f1eq2 bicomd ancom anbi2i
+    cin 3syl sylibr fcoresf1 simprl eqidd simprr anim12d sylc sylbida wfun ffrn
+    impbid2 anbi1d df-f1 3bitr4g 3ad2ant1 f1eq3 3ad2ant3 bitrd anbi2d mpbird ex
+    ax-1 f1cof1 ancoms imaeq2 cnvimarndm eqtrdi eqcoms fdmd eqtrd syl5ib impbid
+    cdm syl ) ABEGZCDFGZEUAZCHZUBZADFEUCZIZABEIZCDFIZJZWMWOWRWMWOJZWQWPWSWQWPJZ
+    WQACEIZJZWMWOEUDZCKZDWNIZXBWMXEWOWMXDAHZWKCUMZCHZJZEXDLZEHZFXGLZFHZJZJZXFXE
+    WOTZWMABCDXDXGEFXJXLWIWJWLUEZXGMZXDMZXJMZWIWJWLUFZXLMZWIWJWLUGUHZXFXHXNNXDA
+    DWNUIZUNUJWMXEJZXIXMXKJZJZXGDXLIZXDXGXJIZJXBWMYGXEWMXOYGYCYFXNXIXMXKUKULUOO
+    YEYIYHYEABCDXDXGEFXJXLWMWIXEXQOXRXSXTWMWJXEYAOYBWMXEPUPQYGYHWQYIXAYGYHWQYGX
+    GCDDXLFXIXMXKUQXIXHYFXFXHPOZYGDURRSYGYIXAYGXDAXGCXJEXIXMXKUSXFXHYFNYJRSUTVA
+    VBWMWTXBTWOWMWPXAWQWMWPAWKEIZXAWIWJWPYKTWLWIWIXCVCZJAWKEGZYLJWPYKWIWIYMYLWI
+    WIYMABEVDWIYMVPVEVFABEVGAWKEVGVHVIWLWIYKXATWJWKCAEVJVKVLVMOVNQVOWRXEWMWOWQW
+    PXEABCDFEVQVRWMXFXPWMXDEWGZAWLWIXDYNHZWJYOCWKCWKHXDXCWKKYNCWKXCVSEVTWAWBVKW
+    MABEXQWCWDYDWHWEWF $.
+
+  $( If the domain of a function ` G ` is a subset of the range of a function
+     ` F ` , then the composition ` ( G o. F ) ` is surjective iff ` G ` is
+     surjective.  (Contributed by GL and AV, 29-Sep-2024.) $)
+  funfocofob $p |- ( ( Fun F /\ G : A --> B /\ A C_ ran F )
+            -> ( ( G o. F ) : ( `' F " A ) -onto-> B <-> G : A -onto-> B ) ) $=
+    ( wfun wf crn wss w3a ccnv wfo cres wa cdm biimpi adantr eqid simpr ex wceq
+    cima ccom cin fdmrn 3ad2ant1 simp2 fcoresfo sseqin2 3ad2ant3 eqtr4d reseq2d
+    fdmd wrel freld resdm syl eqtrd eqidd foeq123d sylibd simpl1 simpl3 syl3anc
+    focofo impbid ) CEZABDFZACGZHZIZCJAUAZBDCUBKZABDKZVJVLVHAUCZBDVNLZKZVMVJVLV
+    PVJVLMCNZVHABVKVNCDCVKLZVOVJVQVHCFZVLVFVGVSVIVFVSCUDOUEPVNQVKQVRQVJVGVLVFVG
+    VIUFZPVOQVJVLRUGSVJVNABBVODVJVODDNZLZDVJVNWADVJVNAWAVIVFVNATZVGVIWCAVHUHOUI
+    ZVJABDVTULUJUKVJDUMWBDTVJABDVTUNDUOUPUQWDVJBURUSUTVJVMVLVJVMMVMVFVIVLVJVMRV
+    FVGVIVMVAVFVGVIVMVBABDCVDVCSVE $.
+
+  $( If the domain of a function ` G ` equals the range of a function ` F ` ,
+     then the composition ` ( G o. F ) ` is surjective iff ` G ` is surjective.
+     (Contributed by GL and AV, 29-Sep-2024.) $)
+  fnfocofob $p |- ( ( F Fn A /\ G : B --> C /\ ran F = B )
+                  -> ( ( G o. F ) : A -onto-> C <-> G : B -onto-> C ) ) $=
+    ( wfn wf crn wceq w3a ccom wfo ccnv cima wb cdm cnvimarndm 3ad2ant1 eqtr2id
+    fndm imaeq2 3ad2ant3 eqtrd foeq2 syl wss fnfun id eqimss2 funfocofob syl3an
+    wfun bitrd ) DAFZBCEGZDHZBIZJZACEDKZLZDMZBNZCUSLZBCELZURAVBIUTVCOURAVAUPNZV
+    BURVEDPZADQUNUOVFAIUQADTRSUQUNVEVBIUOUPBVAUAUBUCAVBCUSUDUEUNDULUOUOUQBUPUFV
+    CVDOADUGUOUHBUPUIBCDEUJUKUM $.
+
+  $( If the domain of a function ` G ` equals the range of a function ` F ` ,
+     then the composition ` ( G o. F ) ` is surjective iff ` G ` and ` F ` as
+     function to the domain of ` G ` are both surjective.  Symmetric version of
+     ~ fnfocofob including the fact that ` F ` is a surjection onto its range.
+     (Contributed by GL and AV, 20-Sep-2024.)  (Proof shortened by AV,
+     29-Sep-2024.) $)
   focofob $p |- ( ( F : A --> B /\ G : C --> D /\ ran F = C )
                   -> ( ( G o. F ) : A -onto-> D
                        <-> ( F : A -onto-> C /\ G : C -onto-> D ) ) ) $=
-    ( wf crn wceq w3a ccom wfo wa ccnv cima cres eqid wi ad2antrr foeq123d syld
-    simp1 fcoreslem3 simp2 simp3 f1cof1blem ancom anbi2i sylibr wb foeq2 eqcoms
-    cin adantr ad2antrl simpr fcoresfo ex simprrr simprll simprlr simprrl eqidd
-    anbi12d biimpd expcomd sylbid mpdan mpid foco ancoms impbid1 ) ABEGZCDFGZEH
-    ZCIZJZADFEKZLZACELZCDFLZMZVQVSENCOZVOCUMZEWCPZLZWBVQABCWCWDEWEVMVNVPUBZWDQZ
-    WCQZWEQZUCVQWCAIZWDCIZMZFWDPZFIZWEEIZMZMZVSWFWBRZRVQWMWPWOMZMWRVQABCDWCWDEF
-    WEWNWGWHWIWJVMVNVPUDZWNQZVMVNVPUEUFWQWTWMWOWPUGUHUIVQWRMZVSWCDVRLZWSWMVSXDU
-    JZVQWQWKXEWLXEAWCAWCDVRUKULUNUOXCXDWDDWNLZWSXCXDXFXCXDMABCDWCWDEFWEWNVQVMWR
-    XDWGSWHWIWJVQVNWRXDXASXBXCXDUPUQURXCWFXFWBXCWFXFMWBXCWFVTXFWAXCWCAWDCWEEVQW
-    MWOWPUSVQWKWLWQUTVQWKWLWQVAZTXCWDCDDWNFVQWMWOWPVBXGXCDVCTVDVEVFUAVGVHVIWAVT
-    VSACDFEVJVKVL $.
+    ( wf crn wceq w3a ccom wfo wa wfn wb ffn fnfocofob syl3an1 dffn4 sylib
+    3ad2ant1 foeq3 3ad2ant3 mpbid biantrurd bitrd ) ABEGZCDFGZEHZCIZJZADFEKLZCD
+    FLZACELZUMMUGEANZUHUJULUMOABEPZACDEFQRUKUNUMUKAUIELZUNUGUHUQUJUGUOUQUPAESTU
+    AUJUGUQUNOUHUICAEUBUCUDUEUF $.
 
   $( If the range of ` F ` equals the domain of ` G ` , then the composition
      ` ( G o. F ) ` is bijective iff ` F ` and ` G ` are both bijective.
-     (Contributed by GL and AV, 20-Sep-2024.) $)
+     (Contributed by GL and AV, 7-Oct-2024.) $)
   f1ocof1ob $p |- ( ( F : A --> B /\ G : C --> D /\ ran F = C )
+                    -> ( ( G o. F ) : A -1-1-onto-> D
+                      <-> ( F : A -1-1-> C /\ G : C -1-1-onto-> D ) ) ) $=
+    ( wf crn wceq w3a ccom wf1 wfo wa wf1o wb ffrn 3ad2ant1 feq3 df-f1o f1cof1b
+    3ad2ant3 mpbid syld3an1 wfn fnfocofob syl3an1 anbi12d bitrdi anbi2i 3bitr4g
+    ffn anass ) ABEGZCDFGZEHZCIZJZADFEKZLZADUSMZNZACELZCDFLZCDFMZNZNZADUSOVCCDF
+    OZNURVBVCVDNZVENVGURUTVIVAVEACEGZUOUNUQUTVIPURAUPEGZVJUNUOVKUQABEQRUQUNVKVJ
+    PUOUPCAESUBUCACCDEFUAUDUNEAUEUOUQVAVEPABEULACDEFUFUGUHVCVDVEUMUIADUSTVHVFVC
+    CDFTUJUK $.
+
+  $( If the range of ` F ` equals the domain of ` G ` , then the composition
+     ` ( G o. F ) ` is bijective iff ` F ` and ` G ` are both bijective.
+     Symmetric version of ~ f1ocof1ob including the fact that ` F ` is a
+     surjection onto its range.  (Contributed by GL and AV, 20-Sep-2024.)
+     (Proof shortened by AV, 7-Oct-2024.) $)
+  f1ocof1ob2 $p |- ( ( F : A --> B /\ G : C --> D /\ ran F = C )
                     -> ( ( G o. F ) : A -1-1-onto-> D
                       <-> ( F : A -1-1-onto-> C /\ G : C -1-1-onto-> D ) ) ) $=
-    ( wf crn wceq w3a ccom wf1 wfo wa wf1o wb wi ffrn feq3 df-f1o f1cof1b com3r
-    3exp sylbid com3l syl 3imp focofob anbi12d an4 bitrdi anbi12i 3bitr4g ) ABE
-    GZCDFGZEHZCIZJZADFEKZLZADUSMZNZACELZACEMZNZCDFLZCDFMZNZNZADUSOACEOZCDFOZNUR
-    VBVCVFNZVDVGNZNVIURUTVLVAVMUNUOUQUTVLPZUNAUPEGZUOUQVNQQABERUQVOUOVNUQVOACEG
-    ZUOVNQUPCAESVPUOUQVNVPUOUQVNACCDEFUAUCUBUDUEUFUGABCDEFUHUIVCVFVDVGUJUKADUST
-    VJVEVKVHACETCDFTULUM $.
+    ( wf crn wceq w3a ccom wf1o wf1 wa f1ocof1ob f1f1orn f1oeq3 syl5ib 3ad2ant3
+    wi f1of1 impbid1 anbi1d bitrd ) ABEGZCDFGZEHZCIZJZADFEKLACEMZCDFLZNACELZUKN
+    ABCDEFOUIUJULUKUIUJULUHUEUJULTUFUJAUGELUHULACEPUGCAEQRSACEUAUBUCUD $.
 
 
 $(