diff --git a/changes-set.txt b/changes-set.txt index be36225cb1..4c4b20eecb 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -105,6 +105,7 @@ Date Old New Notes 16-Sep-25 ismhp [same] Removed unneeded hypotheses 16-Sep-25 selvval [same] Removed unneeded hypotheses 16-Sep-25 mplelsfi [same] Removed unused hypothesis +16-Sep-25 reueqdv [same] Moved from GG's mathbox to main set.mm 11-Sep-25 cascl [same] revised - algSc may be non-injective 10-Sep-25 soeq12d [same] Moved from SO's mathbox to main set.mm 10-Sep-25 freq12d [same] Moved from SO's mathbox to main set.mm diff --git a/discouraged b/discouraged index 4263c70fc6..d0cc359d58 100644 --- a/discouraged +++ b/discouraged @@ -14678,6 +14678,7 @@ New usage of "anmp" is discouraged (11 uses). New usage of "aprilfools2025" is discouraged (0 uses). New usage of "archnq" is discouraged (1 uses). New usage of "arglem1N" is discouraged (0 uses). +New usage of "asclelbasALT" is discouraged (0 uses). New usage of "atabs2i" is discouraged (1 uses). New usage of "atabsi" is discouraged (1 uses). New usage of "atbtwnexOLDN" is discouraged (0 uses). @@ -19991,6 +19992,7 @@ Proof modification of "anabss7p1" is discouraged (5 steps). Proof modification of "ancomstVD" is discouraged (22 steps). Proof modification of "anmp" is discouraged (8 steps). Proof modification of "aprilfools2025" is discouraged (116 steps). +Proof modification of "asclelbasALT" is discouraged (84 steps). Proof modification of "avril1" is discouraged (194 steps). Proof modification of "ax1" is discouraged (3 steps). Proof modification of "ax10fromc7" is discouraged (50 steps). diff --git a/set.mm b/set.mm index de95c33edb..99bbdfa3b7 100644 --- a/set.mm +++ b/set.mm @@ -31921,6 +31921,16 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( wceq wreu reueq1 reubidv bitrd ) DEGZACDHACEHBCEHACDEILABCEFJK $. $} + ${ + $d A x $. $d B x $. + reueqdv.1 $e |- ( ph -> A = B ) $. + $( Formula-building rule for restricted existential uniqueness quantifier. + Deduction form. (Contributed by GG, 1-Sep-2025.) $) + reueqdv $p |- ( ph -> ( E! x e. A ps <-> E! x e. B ps ) ) $= + ( wceq wreu wb reueq1 syl ) ADEGBCDHBCEHIFBCDEJK $. + $( $j usage 'reueqdv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $} + ${ rmoeq1f.1 $e |- F/_ x A $. rmoeq1f.2 $e |- F/_ x B $. @@ -284126,7 +284136,7 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, $( Algebraic span function. $) casp $a class AlgSpan $. - $( Class of algebra scalars function. $) + $( Class of algebra scalar lifting function. $) cascl $a class algSc $. ${ @@ -284538,8 +284548,8 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, asclfval.k $e |- K = ( Base ` F ) $. asclfval.s $e |- .x. = ( .s ` W ) $. asclfval.o $e |- .1. = ( 1r ` W ) $. - $( Function value of the algebra scalars function. (Contributed by Mario - Carneiro, 8-Mar-2015.) $) + $( Function value of the algebra scalar lifting function. (Contributed by + Mario Carneiro, 8-Mar-2015.) $) asclfval $p |- A = ( x e. K |-> ( x .x. .1. ) ) $= ( vw cascl cfv cmpt cbs csca eqtr4di c0 cv cvv wcel wceq cur cvsca fveq2d co fveq2 eqidd oveq123d mpteq12dv df-ascl mptfvmpt wn mpt0 eqtrid mpteq1d @@ -284561,7 +284571,7 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, asclfn.a $e |- A = ( algSc ` W ) $. asclfn.f $e |- F = ( Scalar ` W ) $. asclfn.k $e |- K = ( Base ` F ) $. - $( Unconditional functionality of the algebra scalars function. + $( Unconditional functionality of the algebra scalar lifting function. (Contributed by Mario Carneiro, 9-Mar-2015.) $) asclfn $p |- A Fn K $= ( vx cv cur cfv cvsca co ovex eqid asclfval fnmpti ) HCHIZDJKZDLKZMARSTNH @@ -284577,7 +284587,7 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, ${ asclf.k $e |- K = ( Base ` F ) $. asclf.b $e |- B = ( Base ` W ) $. - $( The algebra scalars function is a function into the base set. + $( The algebra scalar lifting function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015.) $) asclf $p |- ( ph -> A : K --> B ) $= ( vx cv cur cfv cvsca wcel adantr eqid co clmod simpr ringidcl lmodvscl @@ -284586,8 +284596,8 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, NUMDEFGHKUTUSUJUK $. $} - $( The algebra scalars function is a group homomorphism. (Contributed by - Mario Carneiro, 4-Jul-2015.) $) + $( The algebra scalar lifting function is a group homomorphism. + (Contributed by Mario Carneiro, 4-Jul-2015.) $) asclghm $p |- ( ph -> A e. ( F GrpHom W ) ) $= ( vx vy cplusg cfv cbs eqid crg wcel syl co wceq asclval lmodring ringgrp clmod asclf cv cur cvsca adantr simprl simprr ringidcl lmodvsdir syl13anc @@ -284660,7 +284670,7 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, ascldimul.k $e |- K = ( Base ` F ) $. ascldimul.t $e |- .X. = ( .r ` W ) $. ascldimul.s $e |- .x. = ( .r ` F ) $. - $( The algebra scalars function distributes over multiplication. + $( The algebra scalar lifting function distributes over multiplication. (Contributed by Mario Carneiro, 8-Mar-2015.) (Proof shortened by SN, 5-Nov-2023.) $) ascldimul $p |- ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> @@ -284695,8 +284705,8 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, $d x y A $. $d x y F $. $d x y W $. asclrhm.a $e |- A = ( algSc ` W ) $. asclrhm.f $e |- F = ( Scalar ` W ) $. - $( The algebra scalars function is a ring homomorphism. (Contributed by - Mario Carneiro, 8-Mar-2015.) $) + $( The algebra scalar lifting function is a ring homomorphism. + (Contributed by Mario Carneiro, 8-Mar-2015.) $) asclrhm $p |- ( W e. AssAlg -> A e. ( F RingHom W ) ) $= ( vx vy casa wcel cbs cfv cmulr cur assasca assaring assalmod ascl1 cv co eqid wceq ascldimul 3expb asclghm isrhm2d ) CHIZFGBJKZBCBLKZCLKZBMKZACMKZ @@ -292391,7 +292401,7 @@ series in the subring which are also polynomials (in the parent ring). ( crg wcel cid cfv ply1sca2 ply1ring ply1lmod cbs cnx baseid strfvi asclf ) DJKABDLMECGCDFNCDFOCDFPDQRQMESHTIUA $. - $( The value of the algebra scalars function for (univariate) + $( The value of the algebra scalar lifting function for (univariate) polynomials applied to a scalar results in a constant polynomial. (Contributed by AV, 27-Nov-2019.) $) ply1sclcl $p |- ( ( R e. Ring /\ S e. K ) -> ( A ` S ) e. B ) $= @@ -302028,8 +302038,9 @@ are univariate (or multivariate) polynomials. See Wikipedia "Polynomial pmat0opsc.z $e |- .0. = ( 0g ` R ) $. $( The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial - ring embedded into the polynomial ring by the scalar injection/algebraic - scalars function ` algSc ` ). (Contributed by AV, 16-Nov-2019.) $) + ring embedded into the polynomial ring by the scalar injection/algebra + scalar lifting function ` algSc ` ). (Contributed by AV, + 16-Nov-2019.) $) pmat0opsc $p |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) = ( i e. N , j e. N |-> ( A ` .0. ) ) ) $= ( cfn wcel crg wa c0g cfv cmpo eqid pmat0op wceq ply1scl0 eqcomd mpoeq3dv @@ -579829,16 +579840,6 @@ conditions of the Five Segment Axiom ( ~ ax5seg ). See ~ brofs and $( $j usage 'rmoeqbidv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) $} - ${ - $d A x $. $d B x $. - reueqdv.1 $e |- ( ph -> A = B ) $. - $( Formula-building rule for restricted existential uniqueness quantifier. - Deduction form. (Contributed by GG, 1-Sep-2025.) $) - reueqdv $p |- ( ph -> ( E! x e. A ps <-> E! x e. B ps ) ) $= - ( wceq wreu wb reueq1 syl ) ADEGBCDHBCEHIFBCDEJK $. - $( $j usage 'reueqdv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) - $} - ${ $d ph x $. reueqbidv.1 $e |- ( ph -> A = B ) $. @@ -834484,6 +834485,29 @@ additional condition (deduction form). See ~ ralbidc for a more wreu reu5 ) ACBDZAEZSAFZGHABIZHABJZGSAKHABQTUBUAUCABLABMNSAOHABRP $. +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + The universal class +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d x y ph $. $d y ps $. $d x ch $. $d x A $. $d x y B $. $d x y C $. + reuxfr1dd.1 $e |- ( ( ph /\ y e. C ) -> A e. B ) $. + reuxfr1dd.2 $e |- ( ( ph /\ x e. B ) -> E! y e. C x = A ) $. + reuxfr1dd.3 $e |- ( ( ph /\ ( y e. C /\ x = A ) ) -> ( ps <-> ch ) ) $. + $( Transfer existential uniqueness from a variable ` x ` to another + variable ` y ` contained in expression ` A ` . Simplifies ~ reuxfr1d . + (Contributed by Zhi Wang, 20-Sep-2025.) $) + reuxfr1dd $p |- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) ) $= + ( wreu cv wceq wa wrex wcel syl anass bitrd biantrurd wb r19.41v pm5.32da + reurex 3bitr3g rexbidv2 bitr3id adantr reubidva wrmo reurmo reuxfrd ) ABD + GLDMZFNZCOZEHPZDGLCEHLABUQDGAUNGQZOZBUOEHPZBOZUQUSUTBUSUOEHLZUTJUOEHUERUA + AVAUQUBURVAUOBOZEHPAUQUOBEHUCAVCUPEHHAEMHQZUOOZBOVECOVDVCOVDUPOAVEBCKUDVD + UOBSVDUOCSUFUGUHUITUJACDEFGHIUSVBUOEHUKJUOEHULRUMT $. + $} + + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- The empty set @@ -836643,8 +836667,16 @@ have GLB (expanded version). (Contributed by Zhi Wang, asclelbas.w $e |- ( ph -> W e. AssAlg ) $. asclelbas.c $e |- ( ph -> C e. B ) $. $( Lifted scalars are in the base set of the algebra. (Contributed by Zhi - Wang, 11-Sep-2025.) $) + Wang, 11-Sep-2025.) (Proof shortened by Thierry Arnoux, + 22-Sep-2025.) $) asclelbas $p |- ( ph -> ( A ` C ) e. ( Base ` W ) ) $= + ( cbs cfv casa wcel crg assaring syl clmod assalmod eqid asclf ffvelcdmd + ) ACFLMZDBABUDECFGHAFNOZFPOJFQRAUEFSOJFTRIUDUAUBKUC $. + + $( Alternate proof for ~ asclelbas . (Contributed by Zhi Wang, + 11-Sep-2025.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + asclelbasALT $p |- ( ph -> ( A ` C ) e. ( Base ` W ) ) $= ( cfv cur cvsca co cbs wcel wceq eqid syl asclval casa clmod assalmod crg assaring ringidcl 3syl lmodvscld eqeltrd ) ADBLZDFMLZFNLZOZFPLZADCQUKUNRK BUMULECFDGHIUMSZULSZUATADUMECUOFULUOSZHUPIAFUBQZFUCQJFUDTKAUSFUEQULUOQJFU @@ -836653,8 +836685,8 @@ have GLB (expanded version). (Contributed by Zhi Wang, ${ $d A x $. $d C x $. $d M x $. $d W x $. $d ph x $. asclcntr.m $e |- M = ( mulGrp ` W ) $. - $( The algebra scalars function maps into the center of the algebra. - Equivalently, a lifted scalar is a center of the algebra. + $( The algebra scalar lifting function maps into the center of the + algebra. Equivalently, a lifted scalar is a center of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) $) asclcntr $p |- ( ph -> ( A ` C ) e. ( Cntr ` M ) ) $= ( vx cbs cfv eqid wcel co adantr ccntr asclelbas cv wa casa cmulr simpr @@ -836677,7 +836709,7 @@ have GLB (expanded version). (Contributed by Zhi Wang, a "vector" element of ` W ` , of the "scalar" ` C ` , which is now an upper triangular matrix, with the "vector" ` X e. ( Base `` W ) ` . - Equivalently, the algebra scalars function is not necessarily + Equivalently, the algebra scalar lifting function is not necessarily injective unless the algebra is faithful. Therefore, all "scalar injection" was renamed. @@ -836883,12 +836915,93 @@ have GLB (expanded version). (Contributed by Zhi Wang, $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Sections, inverses, isomorphisms +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d .1. g $. $d .x. g $. $d B g $. $d C g $. $d F g $. $d G g $. + $d H g $. $d I g $. $d X g $. $d Y g $. $d g ph $. + isisod.b $e |- B = ( Base ` C ) $. + isisod.h $e |- H = ( Hom ` C ) $. + isisod.o $e |- .x. = ( comp ` C ) $. + isisod.i $e |- I = ( Iso ` C ) $. + isisod.1 $e |- .1. = ( Id ` C ) $. + isisod.c $e |- ( ph -> C e. Cat ) $. + isisod.x $e |- ( ph -> X e. B ) $. + isisod.y $e |- ( ph -> Y e. B ) $. + isisod.f $e |- ( ph -> F e. ( X H Y ) ) $. + isisod.g $e |- ( ph -> G e. ( Y H X ) ) $. + isisod.gf $e |- ( ph -> ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) $. + isisod.fg $e |- ( ph -> ( F ( <. Y , X >. .x. Y ) G ) = ( .1. ` Y ) ) $. + $( The predicate "is an isomorphism" (deduction form). (Contributed by Zhi + Wang, 16-Sep-2025.) $) + isisod $p |- ( ph -> F e. ( X I Y ) ) $= + ( vg co wcel cv cop cfv wceq wa wrex oveq1d eqeq1d oveq2d anbi12d rspcedv + simpr mp2and cco oveqi dfiso2 mpbird ) AFJKIUEUFUDUGZFJKUHZJDUEZUEZJEUIZU + JZFVDKJUHZKDUEZUEZKEUIZUJZUKZUDKJHUEZULZAGFVFUEZVHUJZFGVKUEZVMUJZVQUBUCAV + OVSWAUKUDGVPUAAVDGUJZUKZVIVSVNWAWCVGVRVHWCVDGFVFAWBURZUMUNWCVLVTVMWCVDGFV + KWDUOUNUPUQUSABCEUDFHIVKJKVFLMQORSTPDCUTUIZVEJNVADWEVJKNVAVBVC $. + $} + + ${ + $d .x. k $. $d C k $. $d F k $. $d G k $. $d H k $. $d X k $. + $d Y k $. $d Z k $. $d k ph $. + upeu2lem.b $e |- B = ( Base ` C ) $. + upeu2lem.h $e |- H = ( Hom ` C ) $. + upeu2lem.o $e |- .x. = ( comp ` C ) $. + upeu2lem.i $e |- I = ( Iso ` C ) $. + upeu2lem.c $e |- ( ph -> C e. Cat ) $. + upeu2lem.x $e |- ( ph -> X e. B ) $. + upeu2lem.y $e |- ( ph -> Y e. B ) $. + upeu2lem.z $e |- ( ph -> Z e. B ) $. + upeu2lem.f $e |- ( ph -> F e. ( X I Y ) ) $. + upeu2lem.g $e |- ( ph -> G e. ( X H Z ) ) $. + $( Lemma for ~ upeu2 . There exists a unique morphism from ` Y ` to ` Z ` + that commutes if ` F : X --> Y ` is an isomorphism. (Contributed by Zhi + Wang, 20-Sep-2025.) $) + upeu2lem $p |- ( ph -> E! k e. ( Y H Z ) + G = ( k ( <. X , Y >. .x. Z ) F ) ) $= + ( cinv cfv co wcel cv wceq wb wral wreu isohom eqid invf ffvelcdmd sseldd + cop catcocl wa oveq1 adantl ccid adantr simpr catass cco oveqi isocoinvid + oveq2d catrid 3eqtrd eqtr2d invcoisoid impbida ralrimiva reu6i syl2anc + ccat ) AGFJKCUCUDZUEZUDZKJUQZLDUEZUEZKLHUEZUFGEUGZFJKUQZLDUEZUEZUHZWFWDUH + ZUIZEWEUJWJEWEUKABCDWAGHKJLMNOQSRTAKJIUEZKJHUEZWAABCHIKJMNPQSRULAJKIUEZWM + FVTABCIVSJKMVSUMZQRSPUNUAUOUPZUBURAWLEWEAWFWEUFZUSZWJWKWSWJUSWDWIWAWCUEZW + FWJWDWTUHWSGWIWAWCUTVAWSWTWFUHWJWSWTWFFWAWBKDUEZUEZKKUQLDUEZUEWFKCVBUDZUD + ZXCUEWFWSBCDWAFHWFLKJKMNOACVRUFWRQVCZAKBUFWRSVCZAJBUFWRRVCZXGAWAWNUFWRWQV + CZAFJKHUEZUFWRAWOXJFABCHIJKMNPQRSULUAUPVCZALBUFWRTVCZAWRVDZVEWSXBXEWFXCWS + BCXDFIVSJKXAMPWPXFXHXGAFWOUFWRUAVCZXDUMZDCVFUDZWBKOVGVHVIWSBCDXDWFHKLMNXO + XFXGOXLXMVJVKVCVLWSWKUSWIWDFWHUEZGWKWIXQUHWSWFWDFWHUTVAWSXQGUHWKWSXQGWAFW + GJDUEZUEZJJUQLDUEZUEGJXDUDZXTUEGWSBCDFWAHGLJKJMNOXFXHXGXHXKXIXLAGJLHUEUFW + RUBVCZVEWSXSYAGXTWSBCXDFIVSJKXRMPWPXFXHXGXNXODXPWGJOVGVMVIWSBCDXDGHJLMNXO + XFXHOXLYBVJVKVCVLVNVOWJEWEWDVPVQ $. + $} + + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- Functors -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) + ${ + funcrcl2.f $e |- ( ph -> F ( D Func E ) G ) $. + $( Reverse closure for a functor. (Contributed by Zhi Wang, + 17-Sep-2025.) $) + funcrcl2 $p |- ( ph -> D e. Cat ) $= + ( ccat wcel cfunc co wbr cop wa df-br biimpi funcrcl 3syl simpld ) ABGHZC + GHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $. + + $( Reverse closure for a functor. (Contributed by Zhi Wang, + 17-Sep-2025.) $) + funcrcl3 $p |- ( ph -> E e. Cat ) $= + ( ccat wcel cfunc co wbr cop wa df-br biimpi funcrcl 3syl simprd ) ABGHZC + GHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $. + $} + ${ $d B x y z $. $d F x y z $. $d G x y z $. $d H x y z $. $d J x y z $. $( A utility theorem for proving equivalence of "is a functor". @@ -836907,6 +837020,196 @@ have GLB (expanded version). (Contributed by Zhi Wang, $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Universal property +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d B y $. $d F k m $. $d F l m $. $d F k n y $. $d G k m $. + $d G l m $. $d G k n y $. $d H k m $. $d H l m $. $d H k n y $. + $d J n y $. $d M k m $. $d M l m $. $d M k n y $. $d N k m $. + $d N l m $. $d N k n $. $d O k m $. $d O l m $. $d O k n y $. + $d X k m $. $d X l m $. $d X k n y $. $d Y k m $. $d Y l m $. + $d Y k n y $. $d Z k m $. $d Z l m $. $d Z k n y $. + upciclem1.1 $e |- ( ph -> A. y e. B A. n e. ( Z J ( F ` y ) ) + E! k e. ( X H y ) + n = ( ( ( X G y ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` y ) ) M ) ) $. + upciclem1.y $e |- ( ph -> Y e. B ) $. + upciclem1.n $e |- ( ph -> N e. ( Z J ( F ` Y ) ) ) $. + $( Lemma for ~ upcic , ~ upeu , and ~ upeu2 . (Contributed by Zhi Wang, + 16-Sep-2025.) $) + upciclem1 $p |- ( ph -> E! l e. ( X H Y ) + N = ( ( ( X G Y ) ` l ) + ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $= + ( co vm cv cfv cop wceq wreu eqeq1 reubidv wral fveq2 oveq2d oveq2 fveq1d + eqidd oveq123d eqeq2d reueqdv bitrd raleqbidv oveq1d cbvreuvw bitri sylib + rspcdva ) AKDUBZMNGTZUCZJOMFUCUDZNFUCZLTZTZUEZDMNHTZUFZKPUBZVFUCZJVJTZUEZ + PVMUFZAEUBZVKUEZDVMUFZVNEOVIITZKVTKUEWAVLDVMVTKVKUGUHAVTVEMBUBZGTZUCZJVHW + DFUCZLTZTZUEZDMWDHTZUFZEOWGITZUIWBEWCUIBCNWDNUEZWLWBEWMWCWNWGVIOIWDNFUJZU + KWNWLWADWKUFWBWNWJWADWKWNWIVKVTWNWFVGJJWHVJWNWGVIVHLWOUKWNVEWEVFWDNMGULUM + WNJUNUOUPUHWNWADWKVMWDNMHULUQURUSQRVDSVDVNKUAUBZVFUCZJVJTZUEZUAVMUFVSVLWS + DUAVMVEWPUEZVKWRKWTVGWQJVJVEWPVFUJUTUPVAWSVRUAPVMWPVOUEZWRVQKXAWQVPJVJWPV + OVFUJUTUPVAVBVC $. + $} + + ${ + upcic.b $e |- B = ( Base ` D ) $. + upcic.c $e |- C = ( Base ` E ) $. + upcic.h $e |- H = ( Hom ` D ) $. + upcic.j $e |- J = ( Hom ` E ) $. + upcic.o $e |- O = ( comp ` E ) $. + upcic.f $e |- ( ph -> F ( D Func E ) G ) $. + upcic.x $e |- ( ph -> X e. B ) $. + upcic.y $e |- ( ph -> Y e. B ) $. + ${ + upciclem2.z $e |- ( ph -> Z e. B ) $. + upciclem2.w $e |- ( ph -> W e. C ) $. + upciclem2.m $e |- ( ph -> M e. ( W J ( F ` X ) ) ) $. + upciclem2.od $e |- .x. = ( comp ` D ) $. + upciclem2.k $e |- ( ph -> K e. ( X H Y ) ) $. + upciclem2.l $e |- ( ph -> L e. ( Y H Z ) ) $. + upciclem2.nm $e |- ( ph -> N = ( ( ( X G Y ) ` K ) + ( <. W , ( F ` X ) >. O ( F ` Y ) ) M ) ) $. + $( Lemma for ~ upciclem3 and ~ upeu2 . (Contributed by Zhi Wang, + 19-Sep-2025.) $) + upciclem2 $p |- ( ph -> ( ( ( X G Z ) ` ( L ( <. X , Y >. .x. Z ) K ) ) + ( <. W , ( F ` X ) >. O ( F ` Z ) ) M ) + = ( ( ( Y G Z ) ` L ) ( <. W , ( F ` Y ) >. O ( F ` Z ) ) N ) ) $= + ( cfv cop funcrcl3 funcf1 ffvelcdmd funcf2 catass funcco oveq1d 3eqtr4d + co oveq2d ) ALRSHVEZUOZKQRHVEZUOZQGUOZRGUOZUPSGUOZOVEVEZMPVKUPZVMOVEZVE + VHVJMVOVLOVEVEZPVLUPVMOVEZVELKQRUPSEVEVEQSHVEUOZMVPVEVHNVRVEACFOMVJJVHV + MPVKVLUAUCUDADFGHUEUQUIABCQGABCDFGHTUAUEURZUFUSABCRGVTUGUSUJAQRIVEVKVLJ + VEKVIABDFGHIJQRTUBUCUEUFUGUTULUSABCSGVTUHUSARSIVEVLVMJVELVGABDFGHIJRSTU + BUCUEUGUHUTUMUSVAAVSVNMVPABDEFGHIKLOQRSTUBUKUDUEUFUGUHULUMVBVCANVQVHVRU + NVFVD $. + $} + + upcic.z $e |- ( ph -> Z e. C ) $. + upcic.m $e |- ( ph -> M e. ( Z J ( F ` X ) ) ) $. + upcic.1 $e |- ( ph -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w ) + f = ( ( ( X G w ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) ) $. + ${ + $d .x. p $. $d B p w $. $d D p $. $d F f p k w $. $d G f p k w $. + $d H f p k w $. $d J f p w $. $d K p $. $d L p $. $d M f p k w $. + $d O f p k w $. $d X f p k w $. $d Y p $. $d Z f p k w $. + upciclem3.od $e |- .x. = ( comp ` D ) $. + upciclem3.k $e |- ( ph -> K e. ( X H Y ) ) $. + upciclem3.l $e |- ( ph -> L e. ( Y H X ) ) $. + upciclem3.mn $e |- ( ph -> M = ( ( ( Y G X ) ` L ) + ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) $. + upciclem3.nm $e |- ( ph -> N = ( ( ( X G Y ) ` K ) + ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $. + $( Lemma for ~ upciclem4 . (Contributed by Zhi Wang, 17-Sep-2025.) $) + upciclem3 $p |- ( ph -> ( L ( <. X , Y >. .x. X ) K ) + = ( ( Id ` D ) ` X ) ) $= + ( vp cv co cfv wceq ccid fveq2 oveq1d eqeq2d upciclem1 funcrcl2 catcocl + cop eqid catidcl upciclem2 eqtr4d funcid funcf1 ffvelcdmd catlid eqtr2d + funcrcl3 reu2eqd ) APURUSZSSKUTZVAZPUASJVAZVJWERUTZUTZVBPONSTVJSFUTUTZW + CVAZPWFUTZVBPSEVCVAZVAZWCVAZPWFUTZVBURSSLUTWHWLWBWHVBZWGWJPWOWDWIPWFWBW + HWCVDVEVFWBWLVBZWGWNPWPWDWMPWFWBWLWCVDVEVFABCHGJKLMPPRSSUAURULUHUKVGACE + FNOLSTSUBUDUMAEIJKUGVHZUHUIUHUNUOVIACEWKLSUBUDWKVKZWQUHVLAPOTSKUTVAQUAT + JVAVJWERUTUTWJUPACDEFIJKLMNOPQRUASTSUBUCUDUEUFUGUHUIUHUJUKUMUNUOUQVMVNA + WNWEIVCVAZVAZPWFUTPAWMWTPWFACEWKIJKWSSUBWRWSVKZUGUHVOVEADIRWSPMUAWEUCUE + XAAEIJKUGVTUJUFACDSJACDEIJKUBUCUGVPUHVQUKVRVSWA $. + $} + + ${ + $d B p q v $. $d B p q w $. $d D p q r $. $d F f k p q w $. + $d F g l p q v $. $d F p q r $. $d G f k p q w $. $d G g l p q v $. + $d G p q r $. $d H f k p q w $. $d H g l p q v $. $d H p q r $. + $d J f p q w $. $d J g p q v $. $d M f k w $. $d M g l $. + $d M p q r $. $d N f k $. $d N g l v $. $d N p q r $. + $d O f k p q w $. $d O g l p q v $. $d O p q r $. $d X f k p q w $. + $d X g l p q v $. $d X p q r $. $d Y f k p q w $. $d Y g l p q v $. + $d Y p q r $. $d Z f k p q w $. $d Z g l p q v $. $d Z p q r $. + $d p ph q $. + upcic.n $e |- ( ph -> N e. ( Z J ( F ` Y ) ) ) $. + upcic.2 $e |- ( ph -> A. v e. B A. g e. ( Z J ( F ` v ) ) + E! l e. ( Y H v ) + g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) $. + $( Lemma for ~ upcic and ~ upeu . (Contributed by Zhi Wang, + 19-Sep-2025.) $) + upciclem4 $p |- ( ph -> ( X ( ~=c ` D ) Y /\ E. r e. ( X ( Iso ` D ) Y ) + N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) $= + ( vp vq ccic cfv wbr cv co cop wceq ciso wrex wreu upciclem1 reurex syl + wcel wa simpl 3syl eqid cfunc ad2antrr funcrcl2 cco ccid simplrl simprl + simprr simplrr upciclem3 isisod brcici rexlimddv reximssdv fveq2 oveq1d + wral eqeq2d cbvrexvw sylib jca ) ARSFURUSUTZPUAVAZRSLVBZUSZOTRKUSZVCZSK + USZQVBZVBZVDZUARSFVEUSZVBZVFZAPUPVAZWSUSZOXDVBZVDZWQUPRSMVBZAXMUPXNVGXM + UPXNVFABDIGKLMNOPQRSTUPUMUJUNVHXMUPXNVIVJZAXJXNVKZXMVLZVLZOUQVAZSRLVBUS + PTXCVCZXAQVBVBVDZWQUQSRMVBZXRAYAUQYBVGYAUQYBVFAXQVMACDUBHKLMNPOQSRTUQUO + UIULVHYAUQYBVIVNZXRXSYBVKZYAVLZVLZDFXJXGRSXGVOZUCYFFJKLAKLFJVPVBUTXQYEU + HVQZVRZARDVKXQYEUIVQZASDVKXQYEUJVQZYFDFFVSUSZFVTUSZXJXSMXGRSUCUEYLVOZYG + YMVOYIYJYKAXPXMYEWAZXRYDYAWBZYFBDEFYLGIJKLMNXJXSOPQRSTUCUDUEUFUGYHYJYKA + TEVKXQYEUKVQZAOTXANVBVKXQYEULVQAGVAIVARBVAZLVBUSOXBYRKUSZQVBVBVDIRYRMVB + VGGTYSNVBWLBDWLXQYEUMVQYNYOYPXRYDYAWCZAXPXMYEWDZWEYFCDEFYLHUBJKLMNXSXJP + OQSRTUCUDUEUFUGYHYKYJYQAPTXCNVBVKXQYEUNVQAHVAUBVASCVAZLVBUSPXTUUBKUSZQV + BVBVDUBSUUBMVBVGHTUUCNVBWLCDWLXQYEUOVQYNYPYOUUAYTWEWFZWGWHWHAXMUPXHVFXI + AXMXMUPXHXNXOXRYAXJXHVKUQYBYCUUDWHAXPXMWCWIXMXFUPUAXHXJWRVDZXLXEPUUEXKW + TOXDXJWRWSWJWKWMWNWOWP $. + + $( A universal property defines an object up to isomorphism given its + existence. (Contributed by Zhi Wang, 17-Sep-2025.) $) + upcic $p |- ( ph -> X ( ~=c ` D ) Y ) $= + ( vr ccic cfv wbr cv co cop wceq ciso wrex upciclem4 simpld ) ARSFUPUQU + RPUOUSRSLUTUQOTRKUQVASKUQQUTUTVBUORSFVCUQUTVDABCDEFGHIJKLMNOPQRSTUOUAUB + UCUDUEUFUGUHUIUJUKULUMUNVEVF $. + + $( A universal property defines an essentially unique (strong form) pair + of object ` X ` and morphism ` M ` if it exists. (Contributed by Zhi + Wang, 19-Sep-2025.) $) + upeu $p |- ( ph -> E! r e. ( X ( Iso ` D ) Y ) + N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $= + ( cv co cfv cop wceq ciso wrex wrmo wreu ccic wbr upciclem4 simprd eqid + wss funcrcl2 isohom upciclem1 reurmo syl nfcv ssrmof sylc reu5 sylanbrc + ) APUAUPRSLUQUROTRKURUSSKURQUQUQUTZUARSFVAURZUQZVBZWAUAWCVCZWAUAWCVDARS + FVEURVFWDABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKULUMUNUOVGVHAWCRSMUQ + ZVJWAUAWFVCZWEADFMWBRSUCUEWBVIAFJKLUHVKUIUJVLAWAUAWFVDWGABDIGKLMNOPQRST + UAUMUJUNVMWAUAWFVNVOWAUAWCWFUAWCVPUAWFVPVQVRWAUAWCVSVT $. + $} + + ${ + $d B g l p $. $d B w $. $d D l p $. $d E p $. $d F f k w $. + $d F l p $. $d G f k w $. $d G l p $. $d H f k w $. $d H l p $. + $d I p $. $d J f w $. $d J l p $. $d K l p $. $d M f k w $. + $d M l p $. $d N p $. $d O f k w $. $d O l p $. $d X f k w $. + $d X l p $. $d Y l p $. $d Z f k w $. $d Z l p $. $d f g k p v $. + $d g l p ph v $. $d p v w $. + upeu2.i $e |- I = ( Iso ` D ) $. + upeu2.k $e |- ( ph -> K e. ( X I Y ) ) $. + upeu2.n $e |- ( ph -> + N = ( ( ( X G Y ) ` K ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $. + $( Generate new universal morphism through isomorphism from existing + universal object. (Contributed by Zhi Wang, 20-Sep-2025.) $) + upeu2 $p |- ( ph -> ( N e. ( Z J ( F ` Y ) ) /\ + A. v e. B A. g e. ( Z J ( F ` v ) ) + E! l e. ( Y H v ) + g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) ) + $= + ( vp cfv co wcel cv cop wceq wreu wral funcrcl3 funcf1 ffvelcdmd funcf2 + funcrcl2 isohom sseldd catcocl eqeltrd wa adantr simprl simprr cco eqid + upciclem1 ccat ad2antrr simpr upeu2lem fveq2d cfunc wbr upciclem2 eqtrd + oveq1d eqeq2d reuxfr1dd mpbid ralrimivva jca ) ARUBUAKUSZOUTZVAHVBZUCVB + ZUACVBZLUTUSRUBWRVCXBKUSZSUTUTZVDZUCUAXBMUTZVEZHUBXCOUTZVFCDVFARPTUALUT + ZUSZQUBTKUSZVCZWRSUTUTZWSUQAEJSQXJOUBXKWRUEUGUHAFJKLUIVGULADETKADEFJKLU + DUEUIVHZUJVIADEUAKXNUKVIUMATUAMUTZXKWROUTPXIADFJKLMOTUAUDUFUGUIUJUKVJAT + UANUTZXOPADFMNTUAUDUFUOAFJKLUIVKZUJUKVLUPVMZVIVNVOAXGCHDXHAXBDVAZWTXHVA + ZVPZVPZWTURVBZTXBLUTZUSZQXLXCSUTZUTZVDZURTXBMUTZVEXGYBBDIGKLMOQWTSTXBUB + URAGVBIVBTBVBZLUTUSQXLYJKUSZSUTUTVDITYJMUTVEGUBYKOUTVFBDVFYAUNVQAXSXTVR + ZAXSXTVSWBYBYHXEURUCXAPTUAVCXBFVTUSZUTUTZYIXFYBXAXFVAZVPDFYMPXAMTUAXBUD + UFYMWAZAFWCVAZYAYOXQWDATDVAZYAYOUJWDAUADVAZYAYOUKWDYBXSYOYLVQAPXOVAZYAY + OXRWDYBYOWEVNYBYCYIVAZVPDFYMUCPYCMNTUAXBUDUFYPUOAYQYAUUAXQWDAYRYAUUAUJW + DAYSYAUUAUKWDYBXSUUAYLVQAPXPVAYAUUAUPWDYBUUAWEWFYBYOYCYNVDZVPZVPZYGXDWT + UUDYGYNYDUSZQYFUTXDUUDYEUUEQYFUUDYCYNYDYBYOUUBVSWGWLUUDDEFYMJKLMOPXAQRS + UBTUAXBUDUEUFUGUHAKLFJWHUTWIYAUUCUIWDAYRYAUUCUJWDAYSYAUUCUKWDYBXSUUCYLV + QAUBEVAYAUUCULWDAQUBXKOUTVAYAUUCUMWDYPAYTYAUUCXRWDYBYOUUBVRARXMVDYAUUCU + QWDWJWKWMWNWOWPWQ $. + $} + $} + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Examples of categories