From 82f4fcb885f44e86cc9fa400999d0ff3e831dc72 Mon Sep 17 00:00:00 2001 From: avekens Date: Mon, 7 Oct 2024 18:00:42 +0200 Subject: [PATCH] Composition of functions (follow up) Main: * new theorems ~focnvimacdmdm , ~focofo * proof of ~foco shortened * ~rescnvimafod revised AV's Mathbox: * new theorems ~fresfo , ~fcoresf1b , ~fcoresfob , ~fcoresf1ob, +funfocofob, ~fnfocofob * ~fcoresf1 , ~f1ocof1ob revised * proof of ~focofob, ~f1ocof1ob2 shortened --- set.mm | 251 ++++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 170 insertions(+), 81 deletions(-) diff --git a/set.mm b/set.mm index c0ef8ff9b5..d21394a7a8 100644 --- 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 $. $(