diff --git a/changes-set.txt b/changes-set.txt index 3ae4aba786..f92b8cba63 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -103,6 +103,10 @@ Date Old New Notes 27-Sep-24 syldbl2 [same] moved from SP's mathbox to main set.mm 27-Sep-24 fiminre2 [same] moved from GS's mathbox to main set.mm 27-Sep-24 infrefilb [same] moved from GS's mathbox to main set.mm +26-Sep-24 tltnle [same] moved from TA's mathbox to main set.mm +26-Sep-24 tleile [same] moved from TA's mathbox to main set.mm +26-Sep-24 tospos [same] moved from TA's mathbox to main set.mm +25-Sep-24 biadanid [same] moved from TA's mathbox to main set.mm 22-Sep-24 grpcld [same] moved from SN's mathbox to main set.mm 21-Sep-24 sb56 sbalex substitution expressed with 'al' or with 'ex' 21-Sep-24 nanimn dfnan2 mark as an alternative definition diff --git a/discouraged b/discouraged index 0cf769c0aa..2d2c0f9bff 100644 --- a/discouraged +++ b/discouraged @@ -17274,6 +17274,8 @@ New usage of "mpteq12dvOLD" is discouraged (0 uses). New usage of "mptresidOLD" is discouraged (0 uses). New usage of "mptssALT" is discouraged (0 uses). New usage of "mpv" is discouraged (1 uses). +New usage of "mrelatglbALT" is discouraged (0 uses). +New usage of "mrelatlubALT" is discouraged (0 uses). New usage of "mulassnq" is discouraged (10 uses). New usage of "mulasspi" is discouraged (12 uses). New usage of "mulasspr" is discouraged (1 uses). @@ -18013,6 +18015,7 @@ New usage of "polvalN" is discouraged (4 uses). New usage of "poml4N" is discouraged (3 uses). New usage of "poml5N" is discouraged (1 uses). New usage of "poml6N" is discouraged (1 uses). +New usage of "postcposALT" is discouraged (0 uses). New usage of "prcdnq" is discouraged (14 uses). New usage of "prclisacycgr" is discouraged (0 uses). New usage of "predonOLD" is discouraged (0 uses). @@ -20040,6 +20043,8 @@ Proof modification of "mpofunOLD" is discouraged (95 steps). Proof modification of "mpteq12dvOLD" is discouraged (18 steps). Proof modification of "mptresidOLD" is discouraged (28 steps). Proof modification of "mptssALT" is discouraged (57 steps). +Proof modification of "mrelatglbALT" is discouraged (66 steps). +Proof modification of "mrelatlubALT" is discouraged (76 steps). Proof modification of "mulgfvalALT" is discouraged (317 steps). Proof modification of "n0OLD" is discouraged (6 steps). Proof modification of "n0lpligALT" is discouraged (74 steps). @@ -20159,6 +20164,7 @@ Proof modification of "pm2.43bgbi" is discouraged (16 steps). Proof modification of "pm2.43cbi" is discouraged (34 steps). Proof modification of "pm2.61iOLD" is discouraged (13 steps). Proof modification of "poclOLD" is discouraged (270 steps). +Proof modification of "postcposALT" is discouraged (163 steps). Proof modification of "predonOLD" is discouraged (29 steps). Proof modification of "preleqALT" is discouraged (115 steps). Proof modification of "prmdvdssqOLD" is discouraged (62 steps). diff --git a/set.mm b/set.mm index 162cffbf37..d0d1e108a4 100644 --- a/set.mm +++ b/set.mm @@ -7078,6 +7078,16 @@ _praeclarum theorema_ (splendid theorem). (Contributed by NM, ( wb wi wa biadani mpbi ) BACFGABCHFEABCDIJ $. $} + ${ + biadanid.1 $e |- ( ( ph /\ ps ) -> ch ) $. + biadanid.2 $e |- ( ( ph /\ ch ) -> ( ps <-> th ) ) $. + $( Deduction associated with ~ biadani . Add a conjunction to an + equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.) $) + biadanid $p |- ( ph -> ( ps <-> ( ch /\ th ) ) ) $= + ( wa biimpa an32s mpdan jca biimpar anasss impbida ) ABCDGABGZCDEOCDEACBD + ACGZBDFHIJKACDBPBDFLMN $. + $} + $( Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.) $) pm5.1 $p |- ( ( ph /\ ps ) -> ( ph <-> ps ) ) $= @@ -210553,11 +210563,12 @@ is always a subcategory (and it is full, meaning that all morphisms of that does not have pairwise disjoint hom-sets, proved by this theorem combined with ~ setc2obas . Notably, the empty set ` (/) ` is simultaneously an object ( ~ setc2obas ) , an identity morphism from - ` (/) ` to ` (/) ` , and a non-identity morphism from ` (/) ` to - ` 1o ` . See ~ cat1lem and ~ cat1 for a more general statement. This - category is also thin ( ~ setc2othin ), and therefore is "equivalent" to - a preorder (actually a partial order). See ~ prsthinc for more details - on the "equivalence". (Contributed by Zhi Wang, 24-Sep-2024.) $) + ` (/) ` to ` (/) ` ( ~ setcid or ~ thincid ) , and a non-identity + morphism from ` (/) ` to ` 1o ` . See ~ cat1lem and ~ cat1 for a more + general statement. This category is also thin ( ~ setc2othin ), and + therefore is "equivalent" to a preorder (actually a partial order). See + ~ prsthinc for more details on the "equivalence". (Contributed by Zhi + Wang, 24-Sep-2024.) $) setc2ohom $p |- (/) e. ( ( (/) H (/) ) i^i ( (/) H 1o ) ) $= ( c0 co c1o wcel wf f0 wb wtru c2o cvv a1i df2o3 eleqtrri elsetchom mptru mpbir 2oex cpr 0ex prid1 1oex prid2 elini ) EEEBFZEGBFZEUHHZEEEIZEJUJUKKL @@ -216762,6 +216773,39 @@ net proof size (existence part)? $) TPWGWHWSVTIJABVFVGVSWFVTVHTVI $. $} + ${ + $d x y F $. + $( A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) $) + tospos $p |- ( F e. Toset -> F e. Poset ) $= + ( vx vy ctos wcel cpo cv cple cfv wbr wo cbs wral eqid istos simplbi ) AD + EAFEBGZCGZAHIZJRQSJKCALIZMBTMBCTASTNSNOP $. + $} + + ${ + $d x y B $. $d x y X $. $d y Y $. $d x y .<_ $. + tleile.b $e |- B = ( Base ` K ) $. + tleile.l $e |- .<_ = ( le ` K ) $. + $( In a Toset, any two elements are comparable. (Contributed by Thierry + Arnoux, 11-Feb-2018.) $) + tleile $p |- ( ( K e. Toset /\ X e. B /\ Y e. B ) + -> ( X .<_ Y \/ Y .<_ X ) ) $= + ( vx vy ctos wcel w3a cv wbr wo wral wceq breq1 breq2 orbi12d simp2 simp3 + cpo istos simprbi 3ad2ant1 rspc2va syl21anc ) BJKZDAKZEAKZLUJUKHMZIMZCNZU + MULCNZOZIAPHAPZDECNZEDCNZOZUIUJUKUAUIUJUKUBUIUJUQUKUIBUCKUQHIABCFGUDUEUFU + PUTDUMCNZUMDCNZOHIDEAAULDQUNVAUOVBULDUMCRULDUMCSTUMEQVAURVBUSUMEDCSUMEDCR + TUGUH $. + + tltnle.s $e |- .< = ( lt ` K ) $. + $( In a Toset, "less than" is equivalent to the negation of the converse of + "less than or equal to", see ~ pltnle . (Contributed by Thierry Arnoux, + 11-Feb-2018.) $) + tltnle $p |- ( ( K e. Toset /\ X e. B /\ Y e. B ) + -> ( X .< Y <-> -. Y .<_ X ) ) $= + ( ctos wcel w3a wbr wn wa cpo wb tospos pltval3 syl3an1 wo tleile bitr2di + ibar pm5.61 syl bitrd ) CJKZEAKZFAKZLZEFBMZEFDMZFEDMZNZOZUOUHCPKUIUJULUPQ + CRABCDEFGHISTUKUMUNUAZUPUOQACDEFGHUBUQUOUQUOOUPUQUOUDUMUNUEUCUFUG $. + $} + $c 1. $. $c 0. $. $c Lat $. @@ -217123,9 +217167,10 @@ net proof size (existence part)? $) $} ${ - latidm.b $e |- B = ( Base ` K ) $. - latidm.j $e |- .\/ = ( join ` K ) $. - $( Lattice join is idempotent. (Contributed by NM, 8-Oct-2011.) $) + latjidm.b $e |- B = ( Base ` K ) $. + latjidm.j $e |- .\/ = ( join ` K ) $. + $( Lattice join is idempotent. Analogue of ~ unidm . (Contributed by NM, + 8-Oct-2011.) $) latjidm $p |- ( ( K e. Lat /\ X e. B ) -> ( X .\/ X ) = X ) $= ( clat wcel wa cple cfv co eqid simpl latjcl 3anidm23 simpr wbr latref wb latjle12 syl13anc mpbi2and latlej1 latasymd ) CGHZDAHZIZACCJKZDDBLZDEUIMZ @@ -217260,7 +217305,7 @@ net proof size (existence part)? $) ${ latmidm.b $e |- B = ( Base ` K ) $. latmidm.m $e |- ./\ = ( meet ` K ) $. - $( Lattice join is idempotent. ( ~ inidm analog.) (Contributed by NM, + $( Lattice meet is idempotent. Analogue of ~ inidm . (Contributed by NM, 8-Nov-2011.) $) latmidm $p |- ( ( K e. Lat /\ X e. B ) -> ( X ./\ X ) = X ) $= ( clat wcel wa cple cfv co simpl latmcl 3anidm23 simpr wbr latmle1 latref @@ -218640,7 +218685,8 @@ net proof size (existence part)? $) ${ mrelatglb.g $e |- G = ( glb ` I ) $. $( Greatest lower bounds in a Moore space are realized by intersections. - (Contributed by Stefan O'Rear, 31-Jan-2015.) $) + (Contributed by Stefan O'Rear, 31-Jan-2015.) See ~ mrelatglbALT for + an alternate proof. $) mrelatglb $p |- ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> ( G ` U ) = |^| U ) $= ( vx vy cfv wcel wss w3a wceq 3ad2ant1 wa wbr wb ipole syl3anc cmre wne @@ -218668,7 +218714,8 @@ net proof size (existence part)? $) mrelatlub.f $e |- F = ( mrCls ` C ) $. mrelatlub.l $e |- L = ( lub ` I ) $. $( Least upper bounds in a Moore space are realized by the closure of the - union. (Contributed by Stefan O'Rear, 31-Jan-2015.) $) + union. (Contributed by Stefan O'Rear, 31-Jan-2015.) See + ~ mrelatlubALT for an alternate proof. $) mrelatlub $p |- ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( L ` U ) = ( F ` U. U ) ) $= ( vx cfv wcel wss wa wceq adantr wbr wb ipole syl3anc vy cmre cuni cple @@ -218713,7 +218760,7 @@ net proof size (existence part)? $) $( A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO ( ~ df-riota update): Reprove using ~ isclat instead of the isclatBAD. hypothesis. See commented-out - mreclat above. $) + mreclat above. See ~ mreclat for a good version. $) mreclatBAD $p |- ( C e. ( Moore ` X ) -> I e. CLat ) $= ( cmre cfv wcel wss wa wi cuni eqid adantl wceq eqeltrd c0 ad2antrr eleq2 cpo cbs club cglb wal ccla ipopos a1i cmrc mrelatlub uniss mreuni sseqtrd @@ -465526,16 +465573,6 @@ and the expression ( x e. A /\ x e. B ) ` . ( wo w3o df-3or sylbir olcs ) ABFZCDKCFABCGDABCHEIJ $. $} - ${ - biadanid.1 $e |- ( ( ph /\ ps ) -> ch ) $. - biadanid.2 $e |- ( ( ph /\ ch ) -> ( ps <-> th ) ) $. - $( Deduction associated with ~ biadani . Add a conjunction to an - equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.) $) - biadanid $p |- ( ph -> ( ps <-> ( ch /\ th ) ) ) $= - ( wa biimpa an32s mpdan jca biimpar anasss impbida ) ABCDGABGZCDEOCDEACBD - ACGZBDFHIJKACDBPBDFLMN $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -472776,12 +472813,6 @@ Splicing words (substring replacement) $} ${ - $d x y F $. - $( A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) $) - tospos $p |- ( F e. Toset -> F e. Poset ) $= - ( vx vy ctos wcel cpo cv cple cfv wbr wo cbs wral eqid istos simplbi ) AD - EAFEBGZCGZAHIZJRQSJKCALIZMBTMBCTASTNSNOP $. - $d x y z A $. $d x y z F $. $( The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) $) @@ -472813,30 +472844,6 @@ Splicing words (substring replacement) VJVHVIABVQCVFWGWIURZSVDVQVJVIVHWJSUSUTQVADEVNVFVJVNPVJPRVB $. $} - ${ - $d x y B $. $d x y X $. $d y Y $. $d x y .<_ $. - tleile.b $e |- B = ( Base ` K ) $. - tleile.l $e |- .<_ = ( le ` K ) $. - $( In a Toset, two elements must compare. (Contributed by Thierry Arnoux, - 11-Feb-2018.) $) - tleile $p |- ( ( K e. Toset /\ X e. B /\ Y e. B ) - -> ( X .<_ Y \/ Y .<_ X ) ) $= - ( vx vy ctos wcel w3a cv wbr wo wral wceq breq1 breq2 orbi12d simp2 simp3 - cpo istos simprbi 3ad2ant1 rspc2va syl21anc ) BJKZDAKZEAKZLUJUKHMZIMZCNZU - MULCNZOZIAPHAPZDECNZEDCNZOZUIUJUKUAUIUJUKUBUIUJUQUKUIBUCKUQHIABCFGUDUEUFU - PUTDUMCNZUMDCNZOHIDEAAULDQUNVAUOVBULDUMCRULDUMCSTUMEQVAURVBUSUMEDCSUMEDCR - TUGUH $. - - tltnle.s $e |- .< = ( lt ` K ) $. - $( In a Toset, less-than is equivalent to not inverse "less than or equal - to" see ~ pltnle . (Contributed by Thierry Arnoux, 11-Feb-2018.) $) - tltnle $p |- ( ( K e. Toset /\ X e. B /\ Y e. B ) - -> ( X .< Y <-> -. Y .<_ X ) ) $= - ( ctos wcel w3a wbr wn wa cpo wb tospos pltval3 syl3an1 wo tleile bitr2di - ibar pm5.61 syl bitrd ) CJKZEAKZFAKZLZEFBMZEFDMZFEDMZNZOZUOUHCPKUIUJULUPQ - CRABCDEFGHISTUKUMUNUAZUPUOQACDEFGHUBUQUOUQUOOUPUQUOUDUMUNUEUCUFUG $. - $} - ${ $d x y K $. odutos.d $e |- D = ( ODual ` K ) $. @@ -778135,13 +778142,25 @@ coordinates of the intersection points of a (nondegenerate) line and a $} ${ - monepilem.1 $e |- ( ph -> ( ps <-> ( ch /\ th ) ) ) $. - monepilem.2 $e |- ( ( ph /\ ch ) -> th ) $. - $( Common lemmas for proving monomorphisms, epimorphisms, and potentially - others. (Contributed by Zhi Wang, 24-Sep-2024.) $) - monepilem $p |- ( ph -> ( ps <-> ch ) ) $= - ( simprbda ex wa ancld sylibrd impbid ) ABCABCABCDEGHACCDIBACDACDFHJEKL - $. + mpbiran3d.1 $e |- ( ph -> ( ps <-> ( ch /\ th ) ) ) $. + ${ + mpbiran3d.2 $e |- ( ( ph /\ ch ) -> th ) $. + $( Equivalence with a conjunction one of whose conjuncts is a consequence + of the other. Deduction form. (Contributed by Zhi Wang, + 24-Sep-2024.) $) + mpbiran3d $p |- ( ph -> ( ps <-> ch ) ) $= + ( simprbda ex wa ancld sylibrd impbid ) ABCABCABCDEGHACCDIBACDACDFHJEKL + $. + $} + + ${ + mpbiran4d.2 $e |- ( ( ph /\ th ) -> ch ) $. + $( Equivalence with a conjunction one of whose conjuncts is a consequence + of the other. Deduction form. (Contributed by Zhi Wang, + 27-Sep-2024.) $) + mpbiran4d $p |- ( ph -> ( ps <-> th ) ) $= + ( biancomd mpbiran3d ) ABDCABDCEGFH $. + $} $} @@ -778220,6 +778239,19 @@ additional condition (deduction form). See ~ ralbidc for a more ( wa wrex anim1i r19.41v sylibr ) ACGBDEHZCGBCGDEHALCFIBCDEJK $. $} + ${ + $d A x $. $d B x $. $d ch x $. $d ph x $. $d th x $. + rspceb2dv.1 $e |- ( ( ph /\ x e. B ) -> ( ps -> ch ) ) $. + rspceb2dv.2 $e |- ( ( ph /\ ch ) -> A e. B ) $. + rspceb2dv.3 $e |- ( ( ph /\ ch ) -> th ) $. + rspceb2dv.4 $e |- ( x = A -> ( ps <-> th ) ) $. + $( Restricted existential specialization, using implicit substitution in + both directions. (Contributed by Zhi Wang, 28-Sep-2024.) $) + rspceb2dv $p |- ( ph -> ( E. x e. B ps <-> ch ) ) $= + ( wrex rexlimdva wa wcel rspcev syl2anc ex impbid ) ABEGLZCABCEGHMACTACNF + GODTIJBDEFGKPQRS $. + $} + $( Two ways of expressing "at least one" element. (Contributed by Zhi Wang, 23-Sep-2024.) $) rextru $p |- ( E. x x e. A <-> E. x e. A T. ) $= @@ -778349,6 +778381,59 @@ additional condition (deduction form). See ~ ralbidc for a more DEZCBFZGZEZHZBIRUABIHCTJZBIAFCKALRUABMUCUBBCSNOABCPQ $. $} + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + The union of a class +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d A x y $. $d B x y $. + $( Superclass of the greatest lower bound. A dual statement of ~ ssintub . + (Contributed by Zhi Wang, 29-Sep-2024.) $) + unilbss $p |- U. { x e. B | x C_ A } C_ A $= + ( vy cv wss crab cuni unissb wcel sseq1 elrab simprbi mprgbir ) AEZBFZACG + ZHBFDEZBFZDQDQBIRQJRCJSPSARCORBKLMN $. + $} + + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + ZF Set Theory - add the Axiom of Replacement +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Theorems requiring subset and intersection existence +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d A x $. $d B x $. $d V x $. + $( Two ways of expressing a collection of subsets as seen in ~ df-ntr , + ~ unimax , and others (Contributed by Zhi Wang, 27-Sep-2024.) $) + inpw $p |- ( B e. V -> ( A i^i ~P B ) = { x e. A | x C_ B } ) $= + ( wcel cpw cin cv crab wss dfin5 elpw2g rabbidv syl5eq ) CDEZBCFZGAHZPEZA + BIQCJZABIABPKORSABQCDLMN $. + $} + + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + ZF Set Theory - add the Axiom of Power Sets +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Functions +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + ${ $d A g $. $d f g $. $d B f $. $( There is at most one function into the empty set. (Contributed by Zhi @@ -778441,19 +778526,22 @@ additional condition (deduction form). See ~ ralbidc for a more wf ) AFCGAHCIJZCEFZKJZELZMBCDFTDHZAECNUAUEUDBCDOUCUEEBCDUBPQRS $. $} - -$( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - ZF Set Theory - add the Axiom of Power Sets -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -$) - - -$( --.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- - Functions --.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- -$) + ${ + $d A y $. $d B x y $. $d F y $. $d G y $. $d ph y $. + mofeu.1 $e |- G = ( A X. B ) $. + mofeu.2 $e |- ( ph -> ( B = (/) -> A = (/) ) ) $. + mofeu.3 $e |- ( ph -> E* x x e. B ) $. + $( The uniqueness of a function into a set with at most one element. + (Contributed by Zhi Wang, 1-Oct-2024.) $) + mofeu $p |- ( ph -> ( F : A --> B <-> F = G ) ) $= + ( vy c0 wceq wf wb cv wex wa feq3 adantl cxp csn imp f00 rbaib syl eqtrdi + xpeq2 xp0 syl5eq eqeq2d 3bitr4d 19.42v cvv fconst2g bibi12d mpbiri eqeq2i + elv bitr4di exlimiv sylbir wcel wmo wo mo0sn sylib mpjaodan ) ADKLZCDEMZE + FLZNZDJOZUAZLZJPZAVHQZCKEMZEKLZVIVJVPCKLZVQVRNAVHVSHUBVQVRVSCEUCUDUEVHVIV + QNADKCERSVPFKEVHFKLAVHFCDTZKGVHVTCKTKDKCUGCUHUFUISUJUKAVOQAVNQZJPVKAVNJUL + WAVKJVNVKAVNVIEVTLZVJVNVIWBNCVMEMZECVMTZLZNZWFJCVLUMEUNURVNVIWCWBWEDVMCER + VNVTWDEDVMCUGUJUOUPFVTEGUQUSSUTVAABODVBBVCVHVOVDIBJDVEVFVG $. + $} $( If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, @@ -778462,6 +778550,62 @@ additional condition (deduction form). See ~ ralbidc for a more ( cfv wcel c0 wne ne0i wceq fveq1 0fv eqtrdi necon3i syl ) ABCDZEOFGCFGOAHC FOFCFIOBFDFBCFJBKLMN $. + $( A function with non-empty domain is non-empty and has non-empty codomain. + (Contributed by Zhi Wang, 1-Oct-2024.) $) + fdomne0 $p |- ( ( F : X --> Y /\ X =/= (/) ) + -> ( F =/= (/) /\ Y =/= (/) ) ) $= + ( wf c0 wne wa f0dom0 necon3bid biimpa wceq feq3 f00 simprbi syl6bi syl6ibr + wn wi nne imnan sylib necon2ai jca ) BCADZBEFZGZAEFZCEFUDUEUGUDBEAEABCHIJUF + CECEKZUDUEQZRUFQUHUDBEKZUIUHUDBEADZUJCEBALUKAEKUJBAMNOBESPUDUETUAUBUC $. + + $( A function that maps a singleton to a class is injective. (Contributed by + Zhi Wang, 1-Oct-2024.) $) + f1sn2g $p |- ( ( A e. V /\ F : { A } --> B ) -> F : { A } -1-1-> B ) $= + ( wcel csn wf wa wf1 cfv cop wceq fsn2g biimpa simpld f1sng syldan wb f1eq1 + simpl2im mpbird ) ADEZAFZBCGZHZUCBCIZUCBAACJZKFZIZUBUDUGBEZUIUEUJCUHLZUBUDU + JUKHABCDMNZOAUGDBPQUEUJUKUFUIRULUCBCUHSTUA $. + + $( A function that maps the empty set to a class is injective. (Contributed + by Zhi Wang, 1-Oct-2024.) $) + f102g $p |- ( ( A = (/) /\ F : A --> B ) -> F : A -1-1-> B ) $= + ( c0 wceq wf wa wf1 feq2 biimpa f0bi f10 f1eq1 mpbiri sylbi wb f1eq2 adantr + syl mpbird ) ADEZABCFZGZABCHZDBCHZUCDBCFZUEUAUBUFADBCIJUFCDEZUECBKUGUEDBDHB + LDBCDMNOSUAUDUEPUBADBCQRT $. + + ${ + $d A x y $. $d B y $. $d F y $. + $( A function that maps a set with at most one element to a class is + injective. (Contributed by Zhi Wang, 1-Oct-2024.) $) + f1mo $p |- ( ( E* x x e. A /\ F : A --> B ) -> F : A -1-1-> B ) $= + ( vy cv wcel wmo c0 wceq csn wex wo wf wf1 mo0sn f102g wi cvv vex imbi12d + f1sn2g mpan feq2 f1eq2 mpbiri exlimiv imp jaoian sylanb ) AFBGAHBIJZBEFZK + ZJZELZMBCDNZBCDOZAEBPUKUPUQUOBCDQUOUPUQUNUPUQRZEUNURUMCDNZUMCDOZRULSGUSUT + ETULCDSUBUCUNUPUSUQUTBUMCDUDBUMCDUEUAUFUGUHUIUJ $. + $} + + ${ + f002.1 $e |- ( ph -> F : A --> B ) $. + $( A function with an empty codomain must have empty domain. (Contributed + by Zhi Wang, 1-Oct-2024.) $) + f002 $p |- ( ph -> ( B = (/) -> A = (/) ) ) $= + ( wf c0 wceq feq3 f00 simprbi syl6bi syl5com ) ABCDFZCGHZBGHZEONBGDFZPCGB + DIQDGHPBDJKLM $. + $} + + ${ + $d A f $. $d B f $. $d V f $. $d W f $. + map0cor.1 $e |- ( ph -> A e. V ) $. + map0cor.2 $e |- ( ph -> B e. W ) $. + $( A function exists iff an empty codomain is accompanied with an empty + domain. (Contributed by Zhi Wang, 1-Oct-2024.) $) + map0cor $p |- ( ph -> ( ( B = (/) -> A = (/) ) <-> E. f f : A --> B ) ) $= + ( wcel c0 wceq wi cv wf wex wb wa cmap co wn biid necon2bbii imbi2i imnan + wne bitri map0g notbid bitr4id neq0 a1i elmapg exbidv 3bitrd syl2anc ) AC + FIZBEIZCJKZBJKZLZBCDMZNZDOZPHGUPUQQZUTCBRSZJKZTZVAVEIZDOZVCVDUTURBJUEZQZT + ZVGUTURVJTZLVLUSVMURVJBJVJUAUBUCURVJUDUFVDVFVKCBFEUGUHUIVGVIPVDDVEUJUKVDV + HVBDCBVAFEULUMUNUO $. + $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -778626,6 +778770,19 @@ additional condition (deduction form). See ~ ralbidc for a more CDQR $. +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Moore spaces +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + $( The union of a collection of closed sets is a subset. (Contributed by Zhi + Wang, 29-Sep-2024.) $) + mreuniss $p |- ( ( C e. ( Moore ` X ) /\ S C_ C ) -> U. S C_ X ) $= + ( cmre cfv wcel wss wa cuni uniss adantl wceq mreuni adantr sseqtrd ) ACDEF + ZBAGZHBIZAIZCQRSGPBAJKPSCLQACMNO $. + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Topology @@ -779564,12 +779721,686 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Posets and lattices using extensible structures +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Posets +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d .<_ x y z $. $d B x y z $. $d K x y z $. $d S x y z $. + lubeldm2.b $e |- B = ( Base ` K ) $. + lubeldm2.l $e |- .<_ = ( le ` K ) $. + ${ + lubeldm2.u $e |- U = ( lub ` K ) $. + lubeldm2.p $e |- ( ps + <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) $. + lubeldm2.k $e |- ( ph -> K e. Poset ) $. + $( Member of the domain of the least upper bound function of a poset. + (Contributed by Zhi Wang, 26-Sep-2024.) $) + lubeldm2 $p |- ( ph -> ( S e. dom U <-> ( S C_ B /\ E. x e. B ps ) ) ) $= + ( wcel wa cv wbr wral cdm wss wrex cpo lubeldm biimpa reurex anim2i syl + wreu simpl simprl wrmo poslubmo sylan rmobii sylibr anim1ci reu5 anasss + wi biimpar syl12anc impbida ) AGHUAPZGFUBZBCFUCZQZAVEQVFBCFUJZQZVHAVEVJ + ABCDEFGHIJUDKLMNOUEZUFVIVGVFBCFUGUHUIAVHQAVFVIVEAVHUKAVFVGULAVFVGVIAVFQ + ZVGQVGBCFUMZQVIVLVMVGVLDRZCRZJSDGTVNERZJSDGTVOVPJSVAEFTQZCFUMZVMAIUDPVF + VROCDEFGIJLKUNUOBVQCFNUPUQURBCFUSUQUTAVEVJVKVBVCVD $. + $} + + ${ + glbeldm2.g $e |- G = ( glb ` K ) $. + glbeldm2.p $e |- ( ps + <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) $. + glbeldm2.k $e |- ( ph -> K e. Poset ) $. + $( Member of the domain of the greatest lower bound function of a poset. + (Contributed by Zhi Wang, 26-Sep-2024.) $) + glbeldm2 $p |- ( ph -> ( S e. dom G <-> ( S C_ B /\ E. x e. B ps ) ) ) $= + ( wcel wa cv wbr wral cdm wss wrex cpo glbeldm biimpa reurex anim2i syl + wreu simpl simprl wrmo posglbmo sylan rmobii sylibr anim1ci reu5 anasss + wi biimpar syl12anc impbida ) AGHUAPZGFUBZBCFUCZQZAVEQVFBCFUJZQZVHAVEVJ + ABCDEFGHIJUDKLMNOUEZUFVIVGVFBCFUGUHUIAVHQAVFVIVEAVHUKAVFVGULAVFVGVIAVFQ + ZVGQVGBCFUMZQVIVLVMVGVLCRZDRZJSDGTERZVOJSDGTVPVNJSVAEFTQZCFUMZVMAIUDPVF + VROCDEFGIJLKUNUOBVQCFNUPUQURBCFUSUQUTAVEVJVKVBVCVD $. + $} + $} + + ${ + $d K x y z $. $d S x y z $. $d ph x y z $. + lubeldm2d.b $e |- ( ph -> B = ( Base ` K ) ) $. + lubeldm2d.l $e |- ( ph -> .<_ = ( le ` K ) ) $. + ${ + lubeldm2d.u $e |- ( ph -> U = ( lub ` K ) ) $. + lubeldm2d.p $e |- ( ( ph /\ x e. B ) -> ( ps <-> ( A. y e. S y .<_ x /\ + A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) ) $. + lubeldm2d.k $e |- ( ph -> K e. Poset ) $. + $( Member of the domain of the least upper bound function of a poset. + (Contributed by Zhi Wang, 28-Sep-2024.) $) + lubeldm2d $p |- ( ph -> ( S e. dom U + <-> ( S C_ B /\ E. x e. B ps ) ) ) $= + ( cfv wcel wbr wral wa club cdm cbs wss cv cple wrex eqid biid lubeldm2 + wi dmeqd eleq2d sseq2d wb breqd ralbidv imbi12d raleqbidv anbi12d bitrd + adantr pm5.32da anbi1d rexbidv2 3bitr4d ) AGIUAPZUBZQGIUCPZUDZDUEZCUEZI + UFPZRZDGSZVKEUEZVMRZDGSZVLVPVMRZUKZEVISZTZCVIUGZTGHUBZQGFUDZBCFUGZTAWBC + DEVIGVGIVMVIUHVMUHVGUHWBUIOUJAWDVHGAHVGMULUMAWEVJWFWCAFVIGKUNABWBCFVIAV + LFQZBTWGWBTVLVIQZWBTAWGBWBAWGTBVKVLJRZDGSZVKVPJRZDGSZVLVPJRZUKZEFSZTZWB + NAWPWBUOWGAWJVOWOWAAWIVNDGAJVMVKVLLUPUQAWNVTEFVIKAWLVRWMVSAWKVQDGAJVMVK + VPLUPUQAJVMVLVPLUPURUSUTVBVAVCAWGWHWBAFVIVLKUMVDVAVEUTVF $. + $} + + ${ + glbeldm2d.g $e |- ( ph -> G = ( glb ` K ) ) $. + glbeldm2d.p $e |- ( ( ph /\ x e. B ) -> ( ps <-> ( A. y e. S x .<_ y /\ + A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) ) $. + glbeldm2d.k $e |- ( ph -> K e. Poset ) $. + $( Member of the domain of the greatest lower bound function of a poset. + (Contributed by Zhi Wang, 29-Sep-2024.) $) + glbeldm2d $p |- ( ph -> ( S e. dom G + <-> ( S C_ B /\ E. x e. B ps ) ) ) $= + ( cfv wcel wbr wral wa cglb cdm cbs wss cv cple wrex eqid biid glbeldm2 + wi dmeqd eleq2d sseq2d wb breqd ralbidv imbi12d raleqbidv anbi12d bitrd + adantr pm5.32da anbi1d rexbidv2 3bitr4d ) AGIUAPZUBZQGIUCPZUDZCUEZDUEZI + UFPZRZDGSZEUEZVLVMRZDGSZVPVKVMRZUKZEVISZTZCVIUGZTGHUBZQGFUDZBCFUGZTAWBC + DEVIGVGIVMVIUHVMUHVGUHWBUIOUJAWDVHGAHVGMULUMAWEVJWFWCAFVIGKUNABWBCFVIAV + KFQZBTWGWBTVKVIQZWBTAWGBWBAWGTBVKVLJRZDGSZVPVLJRZDGSZVPVKJRZUKZEFSZTZWB + NAWPWBUOWGAWJVOWOWAAWIVNDGAJVMVKVLLUPUQAWNVTEFVIKAWLVRWMVSAWKVQDGAJVMVP + VLLUPUQAJVMVPVKLUPURUSUTVBVAVCAWGWHWBAFVIVKKUMVDVAVEUTVF $. + $} + $} + + ${ + $d G x y z $. $d K x y z $. $d S x y z $. $d T x y z $. $d U x y z $. + $d ph x y z $. + lubsscl.k $e |- ( ph -> K e. Poset ) $. + lubsscl.t $e |- ( ph -> T C_ S ) $. + ${ + lubsscl.u $e |- U = ( lub ` K ) $. + lubsscl.s $e |- ( ph -> S e. dom U ) $. + lubsscl.x $e |- ( ph -> ( U ` S ) e. T ) $. + $( If a subset of ` S ` contains the LUB of ` S ` , then the two sets + have the same LUB. (Contributed by Zhi Wang, 26-Sep-2024.) $) + lubsscl $p |- ( ph -> ( T e. dom U /\ ( U ` T ) = ( U ` S ) ) ) $= + ( vy vx vz wcel cfv cv wbr wral wa cpo cdm wceq cbs wss cple wi lubelss + wrex eqid sstrd sseldd adantr sselda luble ralrimiva w3a breq1 3ad2ant1 + simp3 rspcdva 3expia breq2 ralbidv imbi2d rspcev syl12anc biid lubeldm2 + anbi12d mpbir2and poslubd jca ) ACDUAZNZCDOBDOZUBAVNCEUCOZUDKPZLPZEUEOZ + QZKCRZVQMPZVSQZKCRZVRWBVSQZUFZMVPRZSZLVPUHZACBVPGAVPBDEVSTVPUIZVSUIZHFI + UGUJZAVOVPNVQVOVSQZKCRZWDVOWBVSQZUFZMVPRZWIACVPVOWLJUKZAWMKCAVQCNZSVPBD + EVSTVQWJWKHAETNWSFULABVMNWSIULACBVQGUMUNZUOAWPMVPAWBVPNZWDWOAXAWDUPWCWO + KCVOVQVOWBVSUQAXAWDUSAXAVOCNWDJURUTZVAUOWHWNWQSLVOVPVRVOUBZWAWNWGWQXCVT + WMKCVRVOVQVSVBVCXCWFWPMVPXCWEWOWDVRVOWBVSUQVDVCVIVEVFAWHLKMVPCDEVSWJWKH + WHVGFVHVJAKMVPCVODEVSWKWJHFWLWRWTXBVKVL $. + $} + + ${ + glbsscl.g $e |- G = ( glb ` K ) $. + glbsscl.s $e |- ( ph -> S e. dom G ) $. + glbsscl.x $e |- ( ph -> ( G ` S ) e. T ) $. + $( If a subset of ` S ` contains the GLB of ` S ` , then the two sets + have the same GLB. (Contributed by Zhi Wang, 26-Sep-2024.) $) + glbsscl $p |- ( ph -> ( T e. dom G /\ ( G ` T ) = ( G ` S ) ) ) $= + ( vx vy vz wcel cfv wceq cv wbr wral wa cdm cbs wss cple wi cpo glbelss + wrex eqid sstrd sseldd adantr sselda glble ralrimiva w3a breq2 3ad2ant1 + simp3 rspcdva 3expia breq1 ralbidv imbi2d rspcev syl12anc biid glbeldm2 + anbi12d mpbir2and eqidd cglb a1i posglbd jca ) ACDUAZNZCDOBDOZPAVQCEUBO + ZUCKQZLQZEUDOZRZLCSZMQZWAWBRZLCSZWEVTWBRZUEZMVSSZTZKVSUHZACBVSGAVSBDEWB + UFVSUIZWBUIZHFIUGUJZAVRVSNVRWAWBRZLCSZWGWEVRWBRZUEZMVSSZWLACVSVRWOJUKZA + WPLCAWACNZTVSBDEWBUFWAWMWNHAEUFNXBFULABVPNXBIULACBWAGUMUNZUOAWSMVSAWEVS + NZWGWRAXDWGUPWFWRLCVRWAVRWEWBUQAXDWGUSAXDVRCNWGJURUTZVAUOWKWQWTTKVRVSVT + VRPZWDWQWJWTXFWCWPLCVTVRWAWBVBVCXFWIWSMVSXFWHWRWGVTVRWEWBUQVDVCVIVEVFAW + KKLMVSCDEWBWMWNHWKVGFVHVJALMVSCVRDEWBWNAVSVKDEVLOPAHVMFWOXAXCXEVNVO $. + $} + $} + + ${ + $d .<_ z $. $d B z $. $d X z $. $d Y z $. + lubpr.k $e |- ( ph -> K e. Poset ) $. + lubpr.b $e |- B = ( Base ` K ) $. + lubpr.x $e |- ( ph -> X e. B ) $. + lubpr.y $e |- ( ph -> Y e. B ) $. + lubpr.l $e |- .<_ = ( le ` K ) $. + lubpr.c $e |- ( ph -> X .<_ Y ) $. + lubpr.s $e |- ( ph -> S = { X , Y } ) $. + ${ + lubpr.u $e |- U = ( lub ` K ) $. + $( Lemma for ~ lubprdm and ~ lubpr . (Contributed by Zhi Wang, + 26-Sep-2024.) $) + lubprlem $p |- ( ph -> ( S e. dom U /\ ( U ` S ) = Y ) ) $= + ( vz wcel cfv wbr cdm wceq cpr cv breq1 elrabd cpo posref syl2anc prssd + crab lublecl prid2g syl eqeltrd lubsscl simpld fveq2d simprd 3eqtrd jca + lubid ) ACDUAZRCDSZHUBACGHUCZVCOAVEVCRZVEDSZQUDZHFTZQBUKZDSZUBZAVJVEDEI + AGHVJAVIGHFTQGBVHGHFUEKNUFAVIHHFTZQHBVHHHFUELAEUGRHBRZVMILBEFHJMUHUIUFU + JPAQBDEFHJMPILULAVKHVEAQBDEFHJMPILVBZAVNHVERLGHBUMUNUOUPZUQUOAVDVGVKHAC + VEDOURAVFVLVPUSVOUTVA $. + + $( The set of two comparable elements in a poset has LUB. (Contributed by + Zhi Wang, 26-Sep-2024.) $) + lubprdm $p |- ( ph -> S e. dom U ) $= + ( cdm wcel cfv wceq lubprlem simpld ) ACDQRCDSHTABCDEFGHIJKLMNOPUAUB $. + + $( The LUB of the set of two comparable elements in a poset is the + greater one of the two. (Contributed by Zhi Wang, 26-Sep-2024.) $) + lubpr $p |- ( ph -> ( U ` S ) = Y ) $= + ( cdm wcel cfv wceq lubprlem simprd ) ACDQRCDSHTABCDEFGHIJKLMNOPUAUB $. + $} + + ${ + glbpr.g $e |- G = ( glb ` K ) $. + $( Lemma for ~ glbprdm and ~ glbpr . (Contributed by Zhi Wang, + 26-Sep-2024.) $) + glbprlem $p |- ( ph -> ( S e. dom G /\ ( G ` S ) = X ) ) $= + ( cdm wcel cfv cpo wceq codu club odupos syl odubas oduleval wbr brcnvg + ccnv eqid syl2anc mpbird cpr prcom eqtrdi lubprdm odulub dmeqd eleqtrrd + wb fveq1d lubpr eqtrd jca ) ACDQZRCDSZGUAACEUBSZUCSZQVFABCVIVHFUJZHGAET + RZVHTRIVHEVHUKZUDUEZBVHEVLJUFZLKVHFEVLMUGZAHGVJUHZGHFUHZNAHBRGBRVPVQVAL + KHGBBFUIULUMZACGHUNHGUNOGHUOUPZVIUKZUQADVIAVKDVIUAIVHDETVLPURUEZUSUTAVG + CVISGACDVIWAVBABCVIVHVJHGVMVNLKVOVRVSVTVCVDVE $. + + $( The set of two comparable elements in a poset has GLB. (Contributed by + Zhi Wang, 26-Sep-2024.) $) + glbprdm $p |- ( ph -> S e. dom G ) $= + ( cdm wcel cfv wceq glbprlem simpld ) ACDQRCDSGTABCDEFGHIJKLMNOPUAUB $. + + $( The GLB of the set of two comparable elements in a poset is the less + one of the two. (Contributed by Zhi Wang, 26-Sep-2024.) $) + glbpr $p |- ( ph -> ( G ` S ) = X ) $= + ( cdm wcel cfv wceq glbprlem simprd ) ACDQRCDSGTABCDEFGHIJKLMNOPUAUB $. + $} + $} + + ${ + $d ./\ w x y z $. $d .\/ w x y z $. $d .<_ v $. $d B w x y z $. + $d K v w z $. $d ph x y $. $d v w x y z $. + joindm2.b $e |- B = ( Base ` K ) $. + joindm2.k $e |- ( ph -> K e. V ) $. + ${ + joindm2.u $e |- U = ( lub ` K ) $. + joindm2.j $e |- .\/ = ( join ` K ) $. + $( The join of any two elements always exists iff all unordered pairs + have LUB. (Contributed by Zhi Wang, 25-Sep-2024.) $) + joindm2 $p |- ( ph -> ( dom .\/ = ( B X. B ) + <-> A. x e. B A. y e. B { x , y } e. dom U ) ) $= + ( cdm wss cv wcel wal wb a1i cvv cxp wceq cop wi cpr wral joindmss eqss + baib syl wrel relxp ssrel wa opelxp vex joindef imbi12d 2albidv bitr4di + mp1i r2al 3bitrd ) AFMZDDUAZUBZVEVDNZBOZCOZUCZVEPZVJVDPZUDZCQBQZVHVIUEE + MPZCDUFBDUFZAVDVENZVFVGRADFGHILJUGVFVQVGVDVEUHUIUJVEUKVGVNRADDULBCVEVDU + MVAAVNVHDPVIDPUNZVOUDZCQBQVPAVMVSBCAVKVRVLVOVKVRRAVHVIDDUOSAEFGHTVHVITK + LJVHTPABUPSVITPACUPSUQURUSVOBCDDVBUTVC $. + + joindm3.l $e |- .<_ = ( le ` K ) $. + $( The join of any two elements always exists iff all unordered pairs + have LUB (expanded version). (Contributed by Zhi Wang, + 25-Sep-2024.) $) + joindm3 $p |- ( ph -> ( dom .\/ = ( B X. B ) <-> + A. x e. B A. y e. B E! z e. B ( ( x .<_ z /\ y .<_ z ) /\ + A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) ) $= + ( vv wral wbr wa cdm cxp wceq cv cpr wcel wi wreu joindm2 wss wb simprl + simprr prssd biid lubeldm baibd syldan adantr joinval2lem reubidv bitrd + adantl 2ralbidva ) AHUAFFUBUCBUDZCUDZUEZGUAUFZCFRBFRVEDUDZJSVFVIJSTVEEU + DZJSVFVJJSTVIVJJSZUGEFRTZDFUHZCFRBFRABCFGHIKLMNOUIAVHVMBCFFAVEFUFZVFFUF + ZTZTZVHQUDZVIJSQVGRVRVJJSQVGRVKUGEFRTZDFUHZVMAVPVGFUJZVHVTUKVQVEVFFAVNV + OULZAVNVOUMZUNAVHWAVTAVSDQEFVGGIJKLPNVSUOMUPUQURVPVTVMUKAVPVSVLDFVQDQEF + HIJKVEVFLPOAIKUFVPMUSWBWCUTVAVCVBVDVB $. + $} + + ${ + meetdm2.g $e |- G = ( glb ` K ) $. + meetdm2.m $e |- ./\ = ( meet ` K ) $. + $( The meet of any two elements always exists iff all unordered pairs + have GLB. (Contributed by Zhi Wang, 25-Sep-2024.) $) + meetdm2 $p |- ( ph -> ( dom ./\ = ( B X. B ) + <-> A. x e. B A. y e. B { x , y } e. dom G ) ) $= + ( cdm wss cv wcel wal wb a1i cvv cxp wceq cop wi cpr wral meetdmss eqss + baib syl wrel relxp ssrel wa opelxp vex meetdef imbi12d 2albidv bitr4di + mp1i r2al 3bitrd ) AGMZDDUAZUBZVEVDNZBOZCOZUCZVEPZVJVDPZUDZCQBQZVHVIUEE + MPZCDUFBDUFZAVDVENZVFVGRADFGHILJUGVFVQVGVDVEUHUIUJVEUKVGVNRADDULBCVEVDU + MVAAVNVHDPVIDPUNZVOUDZCQBQVPAVMVSBCAVKVRVLVOVKVRRAVHVIDDUOSAEFGHTVHVITK + LJVHTPABUPSVITPACUPSUQURUSVOBCDDVBUTVC $. + + meetdm3.l $e |- .<_ = ( le ` K ) $. + $( The meet of any two elements always exists iff all unordered pairs + have GLB (expanded version). (Contributed by Zhi Wang, + 25-Sep-2024.) $) + meetdm3 $p |- ( ph -> ( dom ./\ = ( B X. B ) <-> + A. x e. B A. y e. B E! z e. B ( ( z .<_ x /\ z .<_ y ) /\ + A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) ) $= + ( vv wral wbr wa cdm cxp wceq cv cpr wcel wi wreu meetdm2 wss wb simprl + simprr prssd biid glbeldm baibd syldan adantr meetval2lem reubidv bitrd + adantl 2ralbidva ) AJUAFFUBUCBUDZCUDZUEZGUAUFZCFRBFRDUDZVEISVIVFISTEUDZ + VEISVJVFISTVJVIISZUGEFRTZDFUHZCFRBFRABCFGHJKLMNOUIAVHVMBCFFAVEFUFZVFFUF + ZTZTZVHVIQUDZISQVGRVJVRISQVGRVKUGEFRTZDFUHZVMAVPVGFUJZVHVTUKVQVEVFFAVNV + OULZAVNVOUMZUNAVHWAVTAVSDQEFVGGHIKLPNVSUOMUPUQURVPVTVMUKAVPVSVLDFVQDQEF + HIJKVEVFLPOAHKUFVPMUSWBWCUTVAVCVBVDVB $. + $} + $} + + ${ + posjidm.b $e |- B = ( Base ` K ) $. + ${ + posjidm.j $e |- .\/ = ( join ` K ) $. + $( Poset join is idempotent. ~ latjidm could be shortened by this. + (Contributed by Zhi Wang, 27-Sep-2024.) $) + posjidm $p |- ( ( K e. Poset /\ X e. B ) -> ( X .\/ X ) = X ) $= + ( cpo wcel wa cpr club cfv eqid simpl simpr joinval cple posref eqidd + co lubpr eqtrd ) CGHZDAHZIZDDBTDDJZCKLZLDUEUGBCGADDAUGMZFUCUDNZUCUDOZUJ + PUEAUFUGCCQLZDDUIEUJUJUKMZACUKDEULRUEUFSUHUAUB $. + $} + + ${ + posmidm.m $e |- ./\ = ( meet ` K ) $. + $( Poset meet is idempotent. ~ latmidm could be shortened by this. + (Contributed by Zhi Wang, 27-Sep-2024.) $) + posmidm $p |- ( ( K e. Poset /\ X e. B ) -> ( X ./\ X ) = X ) $= + ( cpo wcel wa cpr cglb cfv eqid simpl simpr meetval cple posref eqidd + co glbpr eqtrd ) BGHZDAHZIZDDCTDDJZBKLZLDUEUGBCGADDAUGMZFUCUDNZUCUDOZUJ + PUEAUFUGBBQLZDDUIEUJUJUKMZABUKDEULRUEUFSUHUAUB $. + $} + $} + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Lattices +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d K x y $. + $( A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.) $) + toslat $p |- ( K e. Toset -> K e. Lat ) $= + ( vx vy wcel cpo cfv cdm wceq wa cv cpr wral wbr ad2antrr simplrl simplrr + eqid simpr lubprdm mpjaodan ctos cjn cbs cmee clat tospos club cple eqidd + cxp prcom a1i tleile 3expb ralrimivva joindm2 mpbird cglb glbprdm meetdm2 + wo jca islat sylanbrc ) AUADZAEDZAUBFZGAUCFZVHUJZHZAUDFZGVIHZIAUEDAUFZVEV + JVLVEVJBJZCJZKZAUGFZGDZCVHLBVHLVEVRBCVHVHVEVNVHDZVOVHDZIZIZVNVOAUHFZMZVRV + OVNWCMZWBWDIZVHVPVQAWCVNVOVEVFWAWDVMNZVHQZVEVSVTWDOZVEVSVTWDPZWCQZWBWDRZW + FVPUIZVQQZSWBWEIZVHVPVQAWCVOVNVEVFWAWEVMNZWHVEVSVTWEPZVEVSVTWEOZWKWBWERZV + PVOVNKHWOVNVOUKULZWNSVEVSVTWDWEVAVHAWCVNVOWHWKUMUNZTUOVEBCVHVQVGAEWHVMWNV + GQZUPUQVEVLVPAURFZGDZCVHLBVHLVEXDBCVHVHWBWDXDWEWFVHVPXCAWCVNVOWGWHWIWJWKW + LWMXCQZUSWOVHVPXCAWCVOVNWPWHWQWRWKWSWTXEUSXATUOVEBCVHXCAVKEWHVMXEVKQZUTUQ + VBVHVGAVKWHXBXFVCVD $. + $} + + ${ + $d B s $. $d G s $. $d K t x y z $. $d U s $. $d ph s $. + isclatd.b $e |- ( ph -> B = ( Base ` K ) ) $. + isclatd.u $e |- ( ph -> U = ( lub ` K ) ) $. + isclatd.g $e |- ( ph -> G = ( glb ` K ) ) $. + isclatd.k $e |- ( ph -> K e. Poset ) $. + isclatd.1 $e |- ( ( ph /\ s C_ B ) -> s e. dom U ) $. + isclatd.2 $e |- ( ( ph /\ s C_ B ) -> s e. dom G ) $. + $( The predicate "is a complete lattice" (deduction form). (Contributed by + Zhi Wang, 29-Sep-2024.) $) + isclatd $p |- ( ph -> K e. CLat ) $= + ( vy vx vt vz wcel cv wbr wral cpo club cfv cdm cbs cpw wceq cglb ccla wi + cple wreu crab eqid biid lubdm ssrab2 eqsstrdi wss elpwi sylan2 ralrimiva + wa dfss3 sylibr pweqd dmeqd 3sstr3d eqssd glbdm isclat biimpri syl12anc ) + AEUAQZEUBUCZUDZEUEUCZUFZUGZEUHUCZUDZVRUGZEUIQZJAVPVRAVPMRZNRZEUKUCZSMORZT + WDPRZWFSMWGTWEWHWFSUJPVQTVCZNVQULZOVRUMVRAWINMPVQVOEWFUAOVQUNZWFUNZVOUNZW + IUOJUPWJOVRUQURABUFZCUDZVRVPAFRZWOQZFWNTWNWOUSAWQFWNWPWNQZAWPBUSZWQWPBUTZ + KVAVBFWNWOVDVEABVQGVFZACVOHVGVHVIAWAVRAWAWEWDWFSMWGTWHWDWFSMWGTWHWEWFSUJP + VQTVCZNVQULZOVRUMVRAXBNMPVQVTEWFUAOWKWLVTUNZXBUOJVJXCOVRUQURAWNDUDZVRWAAW + PXEQZFWNTWNXEUSAXFFWNWRAWSXFWTLVAVBFWNXEVDVEXAADVTIVGVHVIWCVNVSWBVCVCVQVO + VTEWKWMXDVKVLVM $. + $} + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Subset order structures +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d A x y z $. $d B x y z $. $d C y z $. + $( Existential uniqueness of the least upper bound. (Contributed by Zhi + Wang, 28-Sep-2024.) $) + intubeu $p |- ( C e. B -> ( ( A C_ C /\ A. y e. B ( A C_ y -> C C_ y ) ) + <-> C = |^| { x e. B | A C_ x } ) ) $= + ( vz wcel wss cv wi wral crab cint wceq ssint sseq2 ralrab bitri biimpri + wa adantl simpll simplr elrabd cbvrabv eleqtrdi intss1 eqssd expl ssintub + syl mpbiri eqimss sylib jca impbid1 ) EDGZCEHZCBIZHZEUSHZJBDKZTECAIZHZADL + ZMZNZUQURVBVGUQURTZVBTZEVFVBEVFHZVHVJVBVJVABVEKVBBEVEOVDUTVABADVCUSCPQRZS + UAVIEVEGVFEHVIECFIZHZFDLVEVIVMURFEDVLECPUQURVBUBUQURVBUCUDVMVDFADVLVCCPUE + UFEVEUGUKUHUIVGURVBVGURCVFHACDUJEVFCPULVGVJVBEVFUMVKUNUOUP $. + + $( Existential uniqueness of the greatest lower bound. (Contributed by Zhi + Wang, 29-Sep-2024.) $) + unilbeu $p |- ( C e. B -> ( ( C C_ A /\ A. y e. B ( y C_ A -> y C_ C ) ) + <-> C = U. { x e. B | x C_ A } ) ) $= + ( vz wcel cv wi wral wa crab cuni wceq sseq1 simpll simplr elrabd cbvrabv + wss eleqtrdi elssuni syl unissb ralrab bitri biimpri adantl eqssd unilbss + expl mpbiri eqimss2 sylib jca impbid1 ) EDGZECTZBHZCTZUSETZIBDJZKEAHZCTZA + DLZMZNZUQURVBVGUQURKZVBKZEVFVIEVEGEVFTVIEFHZCTZFDLVEVIVKURFEDVJECOUQURVBP + UQURVBQRVKVDFADVJVCCOSUAEVEUBUCVBVFETZVHVLVBVLVABVEJVBBVEEUDVDUTVABADVCUS + COUEUFZUGUHUIUKVGURVBVGURVFCTACDUJEVFCOULVGVLVBVFEUMVMUNUOUP $. + $} + + ${ + ipolub.i $e |- I = ( toInc ` F ) $. + ipolub.f $e |- ( ph -> F e. V ) $. + ipolub.s $e |- ( ph -> S C_ F ) $. + ${ + $d F y z $. $d S y $. $d X y z $. $d ph y z $. + ipolublem.l $e |- .<_ = ( le ` I ) $. + $( Lemma for ~ ipolubdm and ~ ipolub . (Contributed by Zhi Wang, + 28-Sep-2024.) $) + ipolublem $p |- ( ( ph /\ X e. F ) + -> ( ( U. S C_ X /\ A. z e. F ( U. S C_ z -> X C_ z ) ) + <-> ( A. y e. S y .<_ X /\ + A. z e. F ( A. y e. S y .<_ z -> X .<_ z ) ) ) ) $= + ( wcel wa wss wbr wral wb ad2antrr cuni cv wi unissb simpr sseldd ipole + simplr syl3anc ralbidva bitr4id adantlr bicomd imbi12d anbi12d ) AIENZO + ZDUAZIPZBUBZIGQZBDRZURCUBZPZIVCPZUCZCERUTVCGQZBDRZIVCGQZUCZCERUQUSUTIPZ + BDRVBBDIUDUQVAVKBDUQUTDNZOZEHNZUTENZUPVAVKSAVNUPVLKTZVMDEUTADEPUPVLLTUQ + VLUEUFZAUPVLUHEFGHUTIJMUGUIUJUKUQVFVJCEUQVCENZOZVDVHVEVIVSVDUTVCPZBDRVH + BDVCUDVSVGVTBDVSVLOVNVOVRVGVTSUQVLVNVRVPULUQVLVOVRVQULUQVRVLUHEFGHUTVCJ + MUGUIUJUKVSVIVEVSVNUPVRVIVESAVNUPVRKTAUPVRUHUQVRUEEFGHIVCJMUGUIUMUNUJUO + $. + $} + + ${ + $d F t v w x y z $. $d I t v w y z $. $d S t v w x y z $. + $d U v w y z $. $d T t v w y z $. $d ph t v w y z $. + ipolub.u $e |- ( ph -> U = ( lub ` I ) ) $. + ipolubdm.t $e |- ( ph -> T = |^| { x e. F | U. S C_ x } ) $. + $( The domain of the LUB of the inclusion poset. (Contributed by Zhi + Wang, 28-Sep-2024.) $) + ipolubdm $p |- ( ph -> ( S e. dom U <-> T e. F ) ) $= + ( vt vz wcel cv wss wa wceq vy cdm cuni wi wral wrex cfv cbs ipobas syl + cple eqidd eqid ipolublem cpo a1i lubeldm2d mpbirand crab cint ad2antrr + ipopos intubeu biimpa adantll eqtr4d eqeltrd simpr biimparc sylan sseq2 + simplr ex sseq1 imbi2d ralbidv anbi12d rspceb2dv bitrd ) ACEUBPZCUCZNQZ + RZWAOQZRZWBWDRZUDZOFUEZSZNFUFZDFPZAVTCFRWJKAWINUAOFCEGGUKUGZAFHPFGUHUGT + JFGHIUIUJAWLULLAUAOCFGWLHWBIJKWLUMUNGUOPAFGIVBUPUQURAWIWKWADRZWEDWDRZUD + ZOFUEZSZNDFAWBFPZSZWIWKWSWISZDWBFWTDWABQRBFUSUTZWBADXATZWRWIMVAWRWIWBXA + TZAWRWIXCBOWAFWBVCVDVEVFAWRWIVLVGVMAWKVHAXBWKWQMWKWQXBBOWAFDVCVIVJWBDTZ + WCWMWHWPWBDWAVKXDWGWOOFXDWFWNWEWBDWDVNVOVPVQVRVS $. + + ipolub.t $e |- ( ph -> T e. F ) $. + $( The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" + could be eliminated with ` S e. dom U ` .) Could be significantly + shortened if ~ poslubdg is in quantified form. ~ mrelatlub could + potentially be shortened using this. See ~ mrelatlubALT . + (Contributed by Zhi Wang, 28-Sep-2024.) $) + ipolub $p |- ( ph -> ( U ` S ) = T ) $= + ( vw vv wcel cv wbr wral vy vz cple cfv eqid cbs wceq ipobas syl ipopos + cpo a1i wa breq1 wi cuni crab cint intubeu biimpar syl2anc wb ipolublem + mpdan mpbid simpld adantr simpr rspcdva ralbidv cbvralvw bitrdi imbi12d + wss breq2 simprd 3impia poslubdg ) AUAUBFCDEGGUCUDZVSUEZAFHQFGUFUDUGJFG + HIUHUILGUKQAFGIUJULKNAUARZCQZUMORZDVSSZWADVSSOCWAWCWADVSUNAWDOCTZWBAWEW + CPRZVSSZOCTZDWFVSSZUOZPFTZACUPZDVNWLWFVNDWFVNUOPFTUMZWEWKUMZADFQZDWLBRV + NBFUQURUGZWMNMWOWMWPBPWLFDUSUTVAAWOWMWNVBNAOPCFGVSHDIJKVTVCVDVEZVFVGAWB + VHVIAUBRZFQZWAWRVSSZUACTZDWRVSSZAWSUMWJXAXBUOPFWRWFWRUGZWHXAWIXBXCWHWCW + RVSSZOCTXAXCWGXDOCWFWRWCVSVOVJXDWTOUACWCWAWRVSUNVKVLWFWRDVSVOVMAWKWSAWE + WKWQVPVGAWSVHVIVQVR $. + $} + + ${ + $d F y z $. $d S y $. $d X y z $. $d ph y z $. + ipoglblem.l $e |- .<_ = ( le ` I ) $. + $( Lemma for ~ ipoglbdm and ~ ipoglb . (Contributed by Zhi Wang, + 29-Sep-2024.) $) + ipoglblem $p |- ( ( ph /\ X e. F ) + -> ( ( X C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ X ) ) + <-> ( A. y e. S X .<_ y /\ + A. z e. F ( A. y e. S z .<_ y -> z .<_ X ) ) ) ) $= + ( wcel wa wss wbr wral wb ad2antrr cint cv wi ssint simplr simpr sseldd + ipole syl3anc ralbidva bitr4id adantlr bicomd imbi12d anbi12d ) AIENZOZ + IDUAZPZIBUBZGQZBDRZCUBZURPZVCIPZUCZCERVCUTGQZBDRZVCIGQZUCZCERUQUSIUTPZB + DRVBBIDUDUQVAVKBDUQUTDNZOZEHNZUPUTENZVAVKSAVNUPVLKTZAUPVLUEVMDEUTADEPUP + VLLTUQVLUFUGZEFGHIUTJMUHUIUJUKUQVFVJCEUQVCENZOZVDVHVEVIVSVDVCUTPZBDRVHB + VCDUDVSVGVTBDVSVLOVNVRVOVGVTSUQVLVNVRVPULUQVRVLUEUQVLVOVRVQULEFGHVCUTJM + UHUIUJUKVSVIVEVSVNVRUPVIVESAVNUPVRKTUQVRUFAUPVRUEEFGHVCIJMUHUIUMUNUJUO + $. + $} + + ${ + $d F t v w x y z $. $d I t v w y z $. $d S t v w x y z $. + $d G v w y z $. $d T t v w y z $. $d ph t v w y z $. + ipoglb.g $e |- ( ph -> G = ( glb ` I ) ) $. + ipoglbdm.t $e |- ( ph -> T = U. { x e. F | x C_ |^| S } ) $. + $( The domain of the GLB of the inclusion poset. (Contributed by Zhi + Wang, 29-Sep-2024.) $) + ipoglbdm $p |- ( ph -> ( S e. dom G <-> T e. F ) ) $= + ( vw vz wcel cv wss wa wceq vy cdm cint wi wral wrex cfv cbs ipobas syl + cple eqidd eqid ipoglblem cpo a1i glbeldm2d mpbirand crab cuni ad2antrr + ipopos unilbeu biimpa adantll eqtr4d eqeltrd simpr biimparc sylan sseq1 + simplr ex sseq2 imbi2d ralbidv anbi12d rspceb2dv bitrd ) ACFUBPZNQZCUCZ + RZOQZWBRZWDWARZUDZOEUEZSZNEUFZDEPZAVTCERWJKAWINUAOECFGGUKUGZAEHPEGUHUGT + JEGHIUIUJAWLULLAUAOCEGWLHWAIJKWLUMUNGUOPAEGIVBUPUQURAWIWKDWBRZWEWDDRZUD + ZOEUEZSZNDEAWAEPZSZWIWKWSWISZDWAEWTDBQWBRBEUSUTZWAADXATZWRWIMVAWRWIWAXA + TZAWRWIXCBOWBEWAVCVDVEVFAWRWIVLVGVMAWKVHAXBWKWQMWKWQXBBOWBEDVCVIVJWADTZ + WCWMWHWPWADWBVKXDWGWOOEXDWFWNWEWADWDVNVOVPVQVRVS $. + + ipoglb.t $e |- ( ph -> T e. F ) $. + $( The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" + could be eliminated with ` S e. dom G ` .) Could be significantly + shortened if ~ posglbd is in quantified form. ~ mrelatglb could + potentially be shortened using this. See ~ mrelatglbALT . + (Contributed by Zhi Wang, 29-Sep-2024.) $) + ipoglb $p |- ( ph -> ( G ` S ) = T ) $= + ( vy vz wcel cv wbr wral vv vw cple cfv eqid cbs wceq ipobas syl ipopos + cpo a1i wa breq2 wi cint crab cuni unilbeu biimpar syl2anc wb ipoglblem + mpdan mpbid simpld adantr simpr rspcdva ralbidv cbvralvw bitrdi imbi12d + wss breq1 simprd 3impia posglbd ) AUAUBECDFGGUCUDZVSUEZAEHQEGUFUDUGJEGH + IUHUILGUKQAEGIUJULKNAUARZCQZUMDORZVSSZDWAVSSOCWAWCWADVSUNAWDOCTZWBAWEPR + ZWCVSSZOCTZWFDVSSZUOZPETZADCUPZVNWFWLVNWFDVNUOPETUMZWEWKUMZADEQZDBRWLVN + BEUQURUGZWMNMWOWMWPBPWLEDUSUTVAAWOWMWNVBNAOPCEGVSHDIJKVTVCVDVEZVFVGAWBV + HVIAUBRZEQZWRWAVSSZUACTZWRDVSSZAWSUMWJXAXBUOPEWRWFWRUGZWHXAWIXBXCWHWRWC + VSSZOCTXAXCWGXDOCWFWRWCVSVOVJXDWTOUACWCWAWRVSUNVKVLWFWRDVSVOVMAWKWSAWEW + KWQVPVGAWSVHVIVQVR $. + $} + $} + + ${ + $d F x y z $. $d G x y z $. $d I x y z $. $d U x y z $. $d V x y z $. + ipoglb0.i $e |- I = ( toInc ` F ) $. + ${ + ipolub0.u $e |- ( ph -> U = ( lub ` I ) ) $. + ipolub0.f $e |- ( ph -> |^| F e. F ) $. + ipolub0.v $e |- ( ph -> F e. V ) $. + $( The LUB of the empty set is the intersection of the base. + (Contributed by Zhi Wang, 30-Sep-2024.) $) + ipolub0 $p |- ( ph -> ( U ` (/) ) = |^| F ) $= + ( vx c0 cint wss 0ss a1i cuni cv crab wceq wcel eqsstri rabeqc eqcomi + uni0 inteqi ipolub ) AJKCLZBCDEFIKCMACNOGUGKPZJQZMZJCRZLSACUKUKCUJJCUJU + ICTUHKUIUDUINUAOUBUCUEOHUF $. + $} + + ${ + ipolub00.u $e |- ( ph -> U = ( lub ` I ) ) $. + ipolub00.f $e |- ( ph -> (/) e. F ) $. + $( The LUB of the empty set is the empty set if it is contained. + (Contributed by Zhi Wang, 30-Sep-2024.) $) + ipolub00 $p |- ( ph -> ( U ` (/) ) = (/) ) $= + ( vy vx vz wcel c0 cfv wceq wa club adantr eqtrd cv wbr cvv cint int0el + syl eqeltrd simpr ipolub0 wn cipo fvprc adantl syl5eq fveq2d fveq1d cdm + wss cple wral wi wrex rex0 intnan base0 eqid biid cpo 0pos a1i lubeldm2 + mtbiri ndmfv pm2.61dan ) ACUAKZLBMZLNAVMOZVNCUBZLVOBCDUAEABDPMZNZVMFQAV + PCKVMAVPLCALCKVPLNZGCUCUDZGUEQAVMUFUGAVSVMVTQRAVMUHZOZVNLLPMZMZLWBLBWCW + BBVQWCAVRWAFQWBDLPWBDCUIMZLEWAWELNACUIUJUKULUMRUNWBLWCUOKZUHWDLNWBWFLLU + PZHSZISZLUQMZTHLURWHJSZWJTHLURWIWKWJTUSJLUROZILUTZOWMWGWLIVAVBWBWLIHJLL + WCLWJVCWJVDWCVDWLVELVFKWBVGVHVIVJLWCVKUDRVL $. + $} + + ${ + ipoglb0.g $e |- ( ph -> G = ( glb ` I ) ) $. + ipoglb0.f $e |- ( ph -> U. F e. F ) $. + $( The GLB of the empty set is the union of the base. (Contributed by + Zhi Wang, 30-Sep-2024.) $) + ipoglb0 $p |- ( ph -> ( G ` (/) ) = U. F ) $= + ( vx c0 cuni cvv wcel uniexr syl wss 0ss a1i cv cint crab wceq ssv int0 + sseqtrri rabeqc unieqi eqcomi ipoglb ) AHIBJZBCDKEAUIBLBKLGBBMNIBOABPQF + UIHRZISZOZHBTZJZUAAUNUIUMBULHBULUJBLUJKUKUJUBUCUDQUEUFUGQGUH $. + $} + $} + + ${ + $d C x y $. $d F x y $. $d G x y $. $d I x y $. $d U x y $. + $d X x y $. + mreclatGOOD.i $e |- I = ( toInc ` C ) $. + ${ + mrelatlubALT.f $e |- F = ( mrCls ` C ) $. + mrelatlubALT.l $e |- L = ( lub ` I ) $. + $( Least upper bounds in a Moore space are realized by the closure of the + union. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened + by Zhi Wang, 29-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + mrelatlubALT $p |- ( ( C e. ( Moore ` X ) /\ U C_ C ) -> + ( L ` U ) = ( F ` U. U ) ) $= + ( vx cmre cfv wcel wss wa cuni simpl simpr wceq syldan club a1i cv crab + cint mreuniss mrcval mrccl ipolub ) AFKLZMZBANZOZJBBPZCLZEADUJGUKULQUKU + LREDUALSUMIUBUKULUNFNZUOUNJUCNJAUDUESABFUFZAUNCFJHUGTUKULUPUOAMUQAUNCFH + UHTUI $. + $} + + ${ + mrelatglbALT.g $e |- G = ( glb ` I ) $. + $( Greatest lower bounds in a Moore space are realized by intersections. + (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Zhi + Wang, 29-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + mrelatglbALT $p |- ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> + ( G ` U ) = |^| U ) $= + ( vx cmre cfv wcel wss c0 wne w3a cint simp1 simp2 cglb wceq a1i unimax + cv crab cuni mreintcl eqcomd syl ipoglb ) AEIJZKZBALZBMNZOZHBBPZACDUJFU + KULUMQUKULUMRCDSJTUNGUAUNUOAKZUOHUCUOLHAUDUEZTABEUFZUPUQUOHUOAUBUGUHURU + I $. + $} + + $( A Moore space is a complete lattice under inclusion. (Contributed by + Zhi Wang, 30-Sep-2024.) $) + mreclat $p |- ( C e. ( Moore ` X ) -> I e. CLat ) $= + ( vx vy cfv wcel eqidd cv wss wa cdm cuni syldan crab cint wceq eqeltrd + c0 cmre club cglb ipobas cpo ipopos cmrc mreuniss eqid mrccl simpl mrcval + a1i simpr ipolubdm mpbird cvv ssv int0 sseqtrri simplr sseqtrrid rabeqcda + inteqd unieqd mreuni mre1cl ad2antrr wne mreintcl unimax 3expa pm2.61dane + w3a syl ipoglbdm isclatd ) ACUAGZHZABUBGZBUCGZBEABVRDUDVSVTIVSWAIBUEHVSAB + DUFUMVSEJZAKZLZWBVTMHWBNZAUGGZGZAHZVSWCWECKZWHAWBCUHZAWEWFCWFUIZUJOWDFWBW + GVTABVRDVSWCUKZVSWCUNZWDVTIVSWCWIWGWEFJZKFAPQRWJAWEWFCFWKULOUOUPWDWBWAMHW + NWBQZKZFAPZNZAHZWDWSWBTWDWBTRZLZWRANZAXAWQAXAWPFAXAWNAHZLZTQZWNWOWNUQXEWN + URUSUTXDWBTWDWTXCVAVDVBVCVEVSXBAHWCWTVSXBCAACVFACVGSVHSVSWCWBTVIZWSVSWCXF + VNZWRWOAXGWOAHWRWORAWBCVJZFWOAVKVOXHSVLVMWDFWBWRAWABVRDWLWMWDWAIWDWRIVPUP + VQ $. + $} + + ${ + $d G x y $. $d I x y $. $d J x y $. $d S x y $. $d U x y $. + topclat.i $e |- I = ( toInc ` J ) $. + $( A topology is a complete lattice under inclusion. (Contributed by Zhi + Wang, 30-Sep-2024.) $) + topclat $p |- ( J e. Top -> I e. CLat ) $= + ( vx vy ctop wcel club cfv cglb ipobas eqidd cv wss cuni uniopn crab cint + cdm mpbird cpo ipopos a1i wa simpl wceq intmin eqcomd syl ipolubdm ssrab2 + simpr sylancl ipoglbdm isclatd ) BFGZBAHIZAJIZADBAFCKUPUQLUPURLAUAGUPBACU + BUCUPDMZBNZUDZUSUQSGUSOZBGZUSBPZVAEUSVBUQBAFCUPUTUEZUPUTULZVAUQLVAVCVBVBE + MZNEBQRZUFVDVCVHVBEVBBUGUHUIUJTVAUSURSGVGUSRNZEBQZOZBGZVAUPVJBNVLVEVIEBUK + VJBPUMVAEUSVKBURAFCVEVFVAURLVAVKLUNTUO $. + + toplatlub.j $e |- ( ph -> J e. Top ) $. + ${ + toplatglb0.g $e |- G = ( glb ` I ) $. + $( The empty intersection in a topology is realized by the base set. + (Contributed by Zhi Wang, 30-Sep-2024.) $) + toplatglb0 $p |- ( ph -> ( G ` (/) ) = U. J ) $= + ( cglb cfv wceq a1i ctop wcel cuni eqid topopn syl ipoglb0 ) ADBCEBCHIJ + AGKADLMDNZDMFDSSOPQR $. + $} + + toplatlub.s $e |- ( ph -> S C_ J ) $. + ${ + toplatlub.u $e |- U = ( lub ` I ) $. + $( Least upper bounds in a topology are realized by unions. (Contributed + by Zhi Wang, 30-Sep-2024.) $) + toplatlub $p |- ( ph -> ( U ` S ) = U. S ) $= + ( vx cuni ctop club cfv wceq a1i wcel cv wss crab uniopn syl2anc intmin + cint eqcomd syl ipolub ) AJBBKZCEDLFGHCDMNOAIPAUHEQZUHUHJRSJETUDZOAELQB + ESUIGHBEUAUBZUIUJUHJUHEUCUEUFUKUG $. + $} + + toplatglb.g $e |- G = ( glb ` I ) $. + toplatglb.e $e |- ( ph -> S =/= (/) ) $. + $( Greatest lower bounds in a topology are realized by the interior of the + intersection. (Contributed by Zhi Wang, 30-Sep-2024.) $) + toplatglb $p |- ( ph -> ( G ` S ) = ( ( int ` J ) ` |^| S ) ) $= + ( vx cfv ctop wceq cuni wss wcel syl syl2anc cvv cint cnt cglb a1i cpw cv + cin crab c0 wne intssuni unissd sstrd eqid ntrval uniexd ssexd inpw eqtrd + unieqd ntropn ipoglb ) AKBBUAZEUBLLZECDMFGHCDUCLNAIUDAVDEVCUEUGZOZKUFVCPK + EUHZOZAEMQZVCEOZPZVDVFNGAVCBOZVJABUIUJVCVLPJBUKRABEHULUMZVCEVJVJUNZUOSAVC + TQZVFVHNAVCVJTAEMGUPVMUQVOVEVGKEVCTURUTRUSAVIVKVDEQGVMVCEVJVNVASVB $. + $} + + ${ + $d A x $. $d B x $. $d J x $. + toplatmeet.i $e |- I = ( toInc ` J ) $. + toplatmeet.j $e |- ( ph -> J e. Top ) $. + toplatmeet.a $e |- ( ph -> A e. J ) $. + toplatmeet.b $e |- ( ph -> B e. J ) $. + ${ + toplatjoin.j $e |- .\/ = ( join ` I ) $. + $( Joins in a topology are realized by unions. (Contributed by Zhi Wang, + 30-Sep-2024.) $) + toplatjoin $p |- ( ph -> ( A .\/ B ) = ( A u. B ) ) $= + ( vx co cpr cfv cpo wcel a1i ctop wceq club cun eqid joinval prssd cuni + ipopos cv wss crab cint uniprg syl2anc unopn syl3anc eqeltrd intmin syl + eqtr2d ipolub eqtrd ) ABCFMBCNZDUAOZOBCUBZAVCFDPEBCEVCUCZKDPQAEDGUGRIJU + DALVBVDVCEDSGHABCEIJUEVCVCTAVERAVBUFZLUHUILEUJUKZVFVDAVFEQVGVFTAVFVDEAB + EQZCEQZVFVDTIJBCEEULUMZAESQVHVIVDEQHIJBCEUNUOZUPLVFEUQURVJUSVKUTVA $. + $} + + ${ + toplatmeet.m $e |- ./\ = ( meet ` I ) $. + $( Meets in a topology are realized by intersections. (Contributed by + Zhi Wang, 30-Sep-2024.) $) + toplatmeet $p |- ( ph -> ( A ./\ B ) = ( A i^i B ) ) $= + ( vx co cpr cfv cpo wcel a1i ctop wceq cglb cin ipopos meetval prssd cv + eqid cint wss crab cuni intprg syl2anc inopn syl3anc eqeltrd unimax syl + eqtr2d ipoglb eqtrd ) ABCFMBCNZDUAOZOBCUBZAVCDFPEBCEVCUGZKDPQAEDGUCRIJU + DALVBVDEVCDSGHABCEIJUEVCVCTAVERALUFVBUHZUILEUJUKZVFVDAVFEQVGVFTAVFVDEAB + EQZCEQZVFVDTIJBCEEULUMZAESQVHVIVDEQHIJBCEUNUOZUPLVFEUQURVJUSVKUTVA $. + $} + $} + + ${ + $d I x y z $. $d J x y z $. + topdlat.i $e |- I = ( toInc ` J ) $. + $( A topology is a distributive lattice under inclusion. (Contributed by + Zhi Wang, 30-Sep-2024.) $) + topdlat $p |- ( J e. Top -> I e. DLat ) $= + ( vx vy vz ctop wcel cv cfv co wceq wral syl cun eleqtrrd eqid toplatmeet + cin syl3anc clat cjn cmee cbs cdlat topclat clatl w3a simpl simpr2 ipobas + ccla wa simpr3 toplatjoin oveq2d simpr1 unopn inopn oveq12d indi 3eqtr4rd + a1i 3eqtrd ralrimivvva isdlat sylanbrc ) BGHZAUAHZDIZEIZFIZAUBJZKZAUCJZKZ + VJVKVOKZVJVLVOKZVMKZLZFAUDJZMEWAMDWAMAUEHVHAULHVIABCUFAUGNVHVTDEFWAWAWAVH + VJWAHZVKWAHZVLWAHZUHZUMZVPVJVKVLOZVOKVJWGSZVSWFVNWGVJVOWFVKVLABVMCVHWEUIZ + WFVKWABVHWBWCWDUJWFVHBWALWIBAGCUKNZPZWFVLWABVHWBWCWDUNWJPZVMQZUOUPWFVJWGA + BVOCWIWFVJWABVHWBWCWDUQWJPZWFVHVKBHZVLBHZWGBHWIWKWLVKVLBURTVOQZRWFVJVKSZV + JVLSZVMKWRWSOZVSWHWFWRWSABVMCWIWFVHVJBHZWOWRBHWIWNWKVJVKBUSTWFVHXAWPWSBHW + IWNWLVJVLBUSTWMUOWFVQWRVRWSVMWFVJVKABVOCWIWNWKWQRWFVJVLABVOCWIWNWLWQRUTWH + WTLWFVJVKVLVAVCVBVDVEDEFWAVMAVOWAQWMWQVFVG $. + $} + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Categories =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Categories +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + ${ $d .<_ w x y z $. $d B w x y z $. $d H w x y z $. $d X w z $. $d Y w z $. @@ -779678,11 +780509,35 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence UCUFUGUHUD $. $} + ${ + $d B f g k $. $d C f g k $. $d H f g k $. $d M f g k $. $d X f g k $. + $d f g k ph $. + endmndlem.b $e |- B = ( Base ` C ) $. + endmndlem.h $e |- H = ( Hom ` C ) $. + endmndlem.o $e |- .x. = ( comp ` C ) $. + endmndlem.c $e |- ( ph -> C e. Cat ) $. + endmndlem.x $e |- ( ph -> X e. B ) $. + endmndlem.m $e |- ( ph -> ( X H X ) = ( Base ` M ) ) $. + endmndlem.p $e |- ( ph -> ( <. X , X >. .x. X ) = ( +g ` M ) ) $. + $( A diagonal hom-set in a category equipped with the restriction of the + composition has a structure of monoid. See also ~ df-mndtc for + converting a monoid to a category. Lemma for ~ bj-endmnd . + (Contributed by Zhi Wang, 25-Sep-2024.) $) + endmndlem $p |- ( ph -> M e. Mnd ) $= + ( vf vg vk cv wcel adantr co cop ccid cfv w3a ccat 3ad2ant1 simp3 catcocl + simp2 simpr3 simpr2 simpr1 catass eqid catidcl simpr catlid catrid ismndd + wa ) AOPQGGEUAZGGUBGDUAFGCUCUDZUDMNAORZVBSZPRZVBSZUEBCDVFVDEGGGHIJAVECUFS + ZVGKUGAVEGBSZVGLUGZVJVJAVEVGUHAVEVGUJUIAVEVGQRZVBSZUEZVABCDVKVFEVDGGGGHIJ + AVHVMKTAVIVMLTZVNVNAVEVGVLUKAVEVGVLULVNAVEVGVLUMUNABCVCEGHIVCUOZKLUPAVEVA + ZBCDVCVDEGGHIVOAVHVEKTZAVIVELTZJVRAVEUQZURVPBCDVCVDEGGHIVOVQVRJVRVSUSUT + $. + $} + $( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- Monomorphisms and epimorphisms -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) ${ @@ -779721,6 +780576,30 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Functors +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $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". + (Contributed by Zhi Wang, 1-Oct-2024.) $) + funcf2lem $p |- ( G e. X_ z e. ( B X. B ) + ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) + <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. x e. B A. y e. B + ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) ) $= + ( cv cfv co cmap wcel wral w3a fveq2 df-ov eqtr4di vex fveq2d cxp cvv wfn + c1st c2nd cixp elixp2 cop wceq op1std op2ndd oveq12d eleq12d elmap bitrdi + wf ovex ralxp 3anbi3i bitri ) FCDDUAZCIZUDJZEJZVBUEJZEJZHKZVBGJZLKZUFMFUB + MZFVAUCZVBFJZVIMZCVANZOVJVKAIZBIZGKZVOEJZVPEJZHKZVOVPFKZUPZBDNADNZOCVAVIF + UGVNWCVJVKVMWBCABDDVBVOVPUHZUIZVMWAVTVQLKZMWBWEVLWAVIWFWEVLWDFJWAVBWDFPVO + VPFQRWEVGVTVHVQLWEVDVRVFVSHWEVCVOEVOVPVBASZBSZUJTWEVEVPEVOVPVBWGWHUKTULWE + VHWDGJVQVBWDGPVOVPGQRULUMVTVQWAVRVSHUQVOVPGUQUNUOURUSUT $. + $} + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Examples of categories @@ -779782,6 +780661,25 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence UFUHABCCEFUETUAUBUC $. $} + ${ + $d C f x y $. + $( A thin category is a category. (Contributed by Zhi Wang, + 17-Sep-2024.) $) + thincc $p |- ( C e. ThinCat -> C e. Cat ) $= + ( vf vx vy cthinc wcel ccat cv chom cfv wmo cbs wral eqid isthinc simplbi + co ) AEFAGFBHCHDHAIJZQFBKDALJZMCSMCDSABRSNRNOP $. + + thinccd.c $e |- ( ph -> C e. ThinCat ) $. + $( A thin category is a category (deduction form). (Contributed by Zhi + Wang, 24-Sep-2024.) $) + thinccd $p |- ( ph -> C e. Cat ) $= + ( cthinc wcel ccat thincc syl ) ABDEBFECBGH $. + $} + + $( A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) $) + thincssc $p |- ThinCat C_ Cat $= + ( vc cthinc ccat cv thincc ssriv ) ABCADEF $. + ${ $d B w y z $. $d B x y z $. $d F k l $. $d G l $. $d H f k w $. $d H k l $. $d H f x y z $. $d X f k w $. $d X k l $. $d X f w z $. @@ -779865,6 +780763,53 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence LUODUKUCZUDABCDEFGHIJKLUEUHUMDUFTUGUNUOULUMDUIUQTUJ $. $} + ${ + $d B f g h z $. $d C f g h z $. $d E f g h z $. $d F f g h z $. + $d H f g h z $. $d M f g h z $. $d X f g h z $. $d Y f g h z $. + $d f g h ph z $. + thincid.c $e |- ( ph -> C e. ThinCat ) $. + thincid.b $e |- B = ( Base ` C ) $. + thincid.h $e |- H = ( Hom ` C ) $. + thincid.x $e |- ( ph -> X e. B ) $. + ${ + thincid.i $e |- .1. = ( Id ` C ) $. + thincid.f $e |- ( ph -> F e. ( X H X ) ) $. + $( In a thin category, a morphism from an object to itself is an identity + morphism. (Contributed by Zhi Wang, 24-Sep-2024.) $) + thincid $p |- ( ph -> F = ( .1. ` X ) ) $= + ( cfv thinccd catidcl thincmo2 ) ABCEGDNFGGKKMABCDFGIJLACHOKPIJHQ $. + $} + + thincmon.y $e |- ( ph -> Y e. B ) $. + ${ + thincmon.m $e |- M = ( Mono ` C ) $. + $( In a thin category, all morphisms are monomorphisms. The converse + does not hold. See ~ grptcmon . (Contributed by Zhi Wang, + 24-Sep-2024.) $) + thincmon $p |- ( ph -> ( X M Y ) = ( X H Y ) ) $= + ( vg vz vh co cv wcel wral vf cop cco cfv wceq w3a simpr1 adantr simpr2 + wi simpr3 cthinc thincmo2 a1d ralrimivvva eqid thinccd ismon2 mpbiran2d + wa eqrdv ) AUAFGEQZFGDQZAUARZVBSVDVCSVDNRZORZFUBGCUCUDZQZQVDPRZVHQUEZVE + VIUEZUJZPVFFDQZTNVMTOBTAVLONPBVMVMAVFBSZVEVMSZVIVMSZUFZUTZVKVJVRBCVEVID + VFFAVNVOVPUGAFBSVQKUHAVNVOVPUIAVNVOVPUKIJACULSVQHUHUMUNUOAOBCVGNPVDDEFG + IJVGUPMACHUQKLURUSVA $. + $} + + ${ + thincepi.e $e |- E = ( Epi ` C ) $. + $( In a thin category, all morphisms are epimorphisms. The converse does + not hold. See ~ grptcepi . (Contributed by Zhi Wang, + 24-Sep-2024.) $) + thincepi $p |- ( ph -> ( X E Y ) = ( X H Y ) ) $= + ( vg vz vh co cv wcel wral vf cop cco cfv wceq w3a adantr simpr1 simpr2 + wi simpr3 cthinc thincmo2 a1d ralrimivvva eqid thinccd isepi2 mpbiran2d + wa eqrdv ) AUAFGDQZFGEQZAUARZVBSVDVCSNRZVDFGUBORZCUCUDZQZQPRZVDVHQUEZVE + VIUEZUJZPGVFEQZTNVMTOBTAVLONPBVMVMAVFBSZVEVMSZVIVMSZUFZUTZVKVJVRBCVEVIE + GVFAGBSVQLUGAVNVOVPUHAVNVOVPUIAVNVOVPUKIJACULSVQHUGUMUNUOAOBCVGNPDVDEFG + IJVGUPMACHUQKLURUSVA $. + $} + $} + ${ $d .x. f g k u v w z $. $d .x. g k l u v w z $. $d .x. f g w x y z $. $d B u v w z $. $d B w x y z $. $d F k l $. $d G l $. @@ -779953,17 +780898,262 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence $} ${ - $d C f x y $. - $( A thin category is a category. (Contributed by Zhi Wang, - 17-Sep-2024.) $) - thincc $p |- ( C e. ThinCat -> C e. Cat ) $= - ( vf vx vy cthinc wcel ccat cv chom cfv wmo cbs wral eqid isthinc simplbi - co ) AEFAGFBHCHDHAIJZQFBKDALJZMCSMCDSABRSNRNOP $. + $d C f x y $. $d O f x y $. + oppcthin.o $e |- O = ( oppCat ` C ) $. + $( The opposite category of a thin category is thin. (Contributed by Zhi + Wang, 29-Sep-2024.) $) + oppcthin $p |- ( C e. ThinCat -> O e. ThinCat ) $= + ( vx vy vf cthinc wcel cbs cfv chom wceq eqid oppcbas a1i cv wa wmo ccat + co eqidd simpl simprr simprl thincmo oppchom eleq2i sylibr thincc oppccat + mobii syl isthincd ) AGHZDEAIJZBFBKJZUOBIJLUNUOABCUOMZNOUNUPUAUNDPZUOHZEP + ZUOHZQZQZFPZUTURAKJZTZHZFRVDURUTUPTZHZFRVCUOAFVEUTURUNVBUBUNUSVAUCUNUSVAU + DUQVEMZUEVIVGFVHVFVDAVEBURUTVJCUFUGUKUHUNASHBSHAUIABCUJULUM $. $} - $( A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) $) - thincssc $p |- ThinCat C_ Cat $= - ( vc cthinc ccat cv thincc ssriv ) ABCADEF $. + ${ + $d C f x y $. $d D f x y $. $d J f x y $. $d f ph x y $. + subthinc.1 $e |- D = ( C |`cat J ) $. + subthinc.j $e |- ( ph -> J e. ( Subcat ` C ) ) $. + subthinc.c $e |- ( ph -> C e. ThinCat ) $. + $( A subcategory of a thin category is thin. (Contributed by Zhi Wang, + 30-Sep-2024.) $) + subthinc $p |- ( ph -> D e. ThinCat ) $= + ( vx vy vf cdm cfv cthinc eqid cv wcel wa co wss adantr cbs eqidd subcss1 + subcfn rescbas reschom csn wex wmo csubc cxp simprl simprr subcss2 sseldd + chom wfn thincmo mosssn2 sylib sstr2 eximdv sylc sylibr subccat isthincd + ) AHIDKKZCJDABUALZBCVGDMEVHNZGABVGDFAVGUBUDZAVHBVGDFVJVIUCZUEAVHBCVGDMEVI + GVJVKUFAHOZVGPZIOZVGPZQZQZVLVNDRZJOZUGZSZJUHZVSVRPJUIVQVRVLVNBUPLZRZSZWDV + TSZJUHZWBVQBVGWCDVLVNADBUJLPVPFTADVGVGUKUQVPVJTWCNZAVMVOULZAVMVOUMZUNVQVS + WDPJUIWGVQVHBJWCVLVNABMPVPGTVQVGVHVLAVGVHSVPVKTZWIUOVQVGVHVNWKWJUOVIWHURJ + JWDUSUTWEWFWAJVRWDVTVAVBVCJJVRUSVDABCDEFVEVF $. + $} + + ${ + $d B m w x y z $. $d C m $. $d E m $. $d F m w x y z $. $d G m w z $. + $d H m w x y z $. $d J m w x y z $. $d K m w z $. $d m ph w z $. + functhinclem1.b $e |- B = ( Base ` D ) $. + functhinclem1.c $e |- C = ( Base ` E ) $. + functhinclem1.h $e |- H = ( Hom ` D ) $. + functhinclem1.j $e |- J = ( Hom ` E ) $. + functhinclem1.e $e |- ( ph -> E e. ThinCat ) $. + functhinclem1.f $e |- ( ph -> F : B --> C ) $. + functhinclem1.k $e |- K = ( x e. B , y e. B |-> + ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) $. + functhinclem1.1 $e |- ( ( ph /\ ( z e. B /\ w e. B ) ) + -> ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) ) $. + $( Lemma for ~ functhinc . Given the object part, there is only one + possible morphism part such that the mapped morphism is in its + corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) $) + functhinclem1 $p |- ( ph -> ( ( G e. _V /\ G Fn ( B X. B ) /\ + A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) + <-> G = K ) ) $= + ( vm cvv wcel cxp wfn cv co cfv wf wral w3a wceq simpl simpr2 simpr3 eqid + wa c0 wi adantlr cthinc ad2antrr simprl ffvelrnd simprr mofeu oveq1 fveq2 + thincmo oveq1d xpeq12d oveq2 oveq2d ovex ovmpo adantl eqeq2d 2ralbidva wb + xpex bitr4d simpr fnmpoi eqfnov2 sylancl biimpa syl21anc cmpo fvexi mpoex + cbs eqeltri eleq1 mpbiri fneq1 biimpar 3jca impbida ) AKUDUEZKFFUFZUGZDUH + ZEUHZLUIZXDJUJZXEJUJZMUIZXDXEKUIZUKZEFULDFULZUMZKNUNZAXMUSAXCXLXNAXMUOAXA + XCXLUPAXAXCXLUQAXCUSZXLXNXOXLXJXDXENUIZUNZEFULDFULZXNXOXKXQDEFFXOXDFUEZXE + FUEZUSZUSZXKXJXFXIUFZUNXQYBUCXFXIXJYCYCURAYAXIUTUNXFUTUNVAXCUBVBYBGIUCMXG + XHAIVCUEXCYASVDYBFGXDJAFGJUKXCYATVDZXOXSXTVEVFYBFGXEJYDXOXSXTVGVFPRVKVHYB + XPYCXJYAXPYCUNXOBCXDXEFFBUHZCUHZLUIZYEJUJZYFJUJZMUIZUFZYCNXDYFLUIZXGYIMUI + ZUFYEXDUNZYGYLYJYMYEXDYFLVIYNYHXGYIMYEXDJVJVLVMYFXEUNZYLXFYMXIYFXEXDLVNYO + YIXHXGMYFXEJVJVOVMUAXFXIXDXELVPXGXHMVPWBVQVRVSWCVTXOXCNXBUGZXNXRWAAXCWDBC + FFYKNUAYGYJYEYFLVPYHYIMVPWBWEZDEFFKNWFWGWCZWHWIAXNUSZXAXCXLXNXAAXNXANUDUE + NBCFFYKWJUDUABCFFYKFHWMOWKZYTWLWNKNUDWOWPVRXNXCAXNXCYPYQXBKNWQWPVRZYSAXCX + NXLAXNUOUUAAXNWDXOXLXNYRWRWIWSWT $. + $} + + ${ + $d B x y $. $d F x y $. $d H x y $. $d J x y $. $d X x y $. + $d Y x y $. + functhinclem2.x $e |- ( ph -> X e. B ) $. + functhinclem2.y $e |- ( ph -> Y e. B ) $. + functhinclem2.1 $e |- ( ph -> A. x e. B A. y e. B + ( ( ( F ` x ) J ( F ` y ) ) = (/) -> ( x H y ) = (/) ) ) $. + $( Lemma for ~ functhinc . (Contributed by Zhi Wang, 1-Oct-2024.) $) + functhinclem2 $p |- ( ph -> + ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) ) $= + ( wcel cv cfv co c0 wceq wi wral simpl fveq2d simpr oveq12d eqeq1d oveq12 + wa imbi12d rspc2gv imp syl21anc ) AHDMZIDMZBNZEOZCNZEOZGPZQRZUNUPFPZQRZSZ + CDTBDTZHEOZIEOZGPZQRZHIFPZQRZSZJKLULUMUGVCVJVBVJBCHIDDUNHRZUPIRZUGZUSVGVA + VIVMURVFQVMUOVDUQVEGVMUNHEVKVLUAUBVMUPIEVKVLUCUBUDUEVMUTVHQUNHUPIFUFUEUHU + IUJUK $. + $} + + ${ + $d F n $. $d F x y $. $d H x y $. $d J n $. $d J x y $. $d X n $. + $d X x y $. $d Y n $. $d Y x y $. $d ph x y $. + functhinclem3.x $e |- ( ph -> X e. B ) $. + functhinclem3.y $e |- ( ph -> Y e. B ) $. + functhinclem3.m $e |- ( ph -> M e. ( X H Y ) ) $. + functhinclem3.g $e |- ( ph -> G = ( x e. B , y e. B |-> + ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) ) $. + functhinclem3.1 $e |- ( ph + -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) ) $. + functhinclem3.2 $e |- ( ph -> E* n n e. ( ( F ` X ) J ( F ` Y ) ) ) $. + $( Lemma for ~ functhinc . The mapped morphism is in its corresponding + hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) $) + functhinclem3 $p |- ( ph -> + ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) ) $= + ( co cfv wf cxp wceq cv wa simprl simprr oveq12d fveq2d xpeq12d wcel ovex + cvv xpex a1i ovmpod eqid mofeu mpbird ffvelrnd ) AKLHSZKFTZLFTZISZJKLGSZA + VAVDVEUAVEVAVDUBZUCABCKLDDBUDZCUDZHSZVGFTZVHFTZISZUBVFGUMPAVGKUCZVHLUCZUE + UEZVIVAVLVDVOVGKVHLHAVMVNUFZAVMVNUGZUHVOVJVBVKVCIVOVGKFVPUIVOVHLFVQUIUHUJ + MNVFUMUKAVAVDKLHULVBVCIULUNUOUPAEVAVDVEVFVFUQQRURUSOUT $. + $} + + ${ + functhinc.b $e |- B = ( Base ` D ) $. + functhinc.c $e |- C = ( Base ` E ) $. + functhinc.h $e |- H = ( Hom ` D ) $. + functhinc.j $e |- J = ( Hom ` E ) $. + functhinc.d $e |- ( ph -> D e. Cat ) $. + functhinc.e $e |- ( ph -> E e. ThinCat ) $. + functhinc.f $e |- ( ph -> F : B --> C ) $. + functhinc.k $e |- K = ( x e. B , y e. B |-> + ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) $. + functhinc.1 $e |- ( ph -> A. z e. B A. w e. B + ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) ) $. + ${ + $d B b c m n p $. $d B b c m n u v $. $d B b c w z $. $d B u v x y $. + $d C p $. $d E p $. $d F p $. $d F u v x y $. $d F w z $. + $d G a b c m n p $. $d G a b c m n u v $. $d H n p $. $d H n u v $. + $d H w z $. $d H u v x y $. $d J p $. $d J u v x y $. $d J w z $. + $d K a b c m n p $. $d K a b c m n u v $. $d a b c m n p ph $. + $d a b c w z $. $d ph u v $. + functhinclem4.1 $e |- .1. = ( Id ` D ) $. + functhinclem4.i $e |- I = ( Id ` E ) $. + functhinclem4.x $e |- .x. = ( comp ` D ) $. + functhinclem4.o $e |- O = ( comp ` E ) $. + $( Lemma for ~ functhinc . Other requirements on the morphism part are + automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024.) $) + functhinclem4 $p |- ( ( ph /\ G = K ) -> A. a e. B + ( ( ( a G a ) ` ( .1. ` a ) ) = ( I ` ( F ` a ) ) /\ + A. b e. B A. c e. B A. m e. ( a H b ) A. n e. ( b H c ) + ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) = + ( ( ( b G c ) ` n ) + ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) + ( ( a G b ) ` m ) ) ) ) $= + ( vv vu vp wceq wa cv cfv co cop wral wcel cthinc ad2antrr wf ffvelrnda + adantr simpr ccat catidcl cmpo simplr oveq1 fveq2 oveq1d xpeq12d oveq2d + cxp oveq2 cbvmpov eqtrdi c0 functhinclem2 thincmo functhinclem3 thincid + eqtri wi ad4antr simplrr ffvelrnd simplrl simprl simprr catcocl thinccd + thincmo2 ralrimivva jca ralrimiva ) AOSUTZVAZUAVBZJVCZXHXHOVDVCZXHNVCZQ + VCUTZLVBZKVBZXHUBVBZVEUCVBZIVDVDZXHXPOVDVCZXMXOXPOVDVCZXNXHXOOVDVCZXKXO + NVCZVEXPNVCZTVDVDZUTZLXOXPPVDZVFKXHXOPVDZVFZUCFVFUBFVFZVAUAFXGXHFVGZVAZ + XLYHYJGMQXJRXKAMVHVGZXFYIUIVIZUEUGXGFGXHNAFGNVJZXFUJVLVKZUNYJUQURFUSNOP + RXIXHXHXGYIVMZYOYJFHJPXHUDUFUMAHVNVGZXFYIUHVIYOVOYJOSUQURFFUQVBZURVBZPV + DZYQNVCZYRNVCZRVDZWCZVPZAXFYIVQSBCFFBVBZCVBZPVDZUUENVCZUUFNVCZRVDZWCZVP + UUDUKBCUQURFFUUKUUCYQUUFPVDZYTUUIRVDZWCUUEYQUTZUUGUULUUJUUMUUEYQUUFPVRU + UNUUHYTUUIRUUEYQNVSVTWAUUFYRUTZUULYSUUMUUBUUFYRYQPWDUUOUUIUUAYTRUUFYRNV + SWBWAWEWLWFZYJDEFNPRXHXHYOYOADVBZNVCEVBZNVCRVDWGUTUUQUURPVDWGUTWMEFVFDF + VFZXFYIULVIWHYJGMUSRXKXKYLYNYNUEUGWIWJWKYJYGUBUCFFYJXOFVGZXPFVGZVAZVAZY + DKLYFYEUVCXNYFVGZXMYEVGZVAZVAZGMXRYCRXKYBYJXKGVGUVBUVFYNVIZUVGFGXPNAYMX + FYIUVBUVFUJWNZYJUUTUVAUVFWOZWPZUVGUQURFUSNOPRXQXHXPYJYIUVBUVFYOVIZUVJUV + GFHIXNXMPXHXOXPUDUFUOAYPXFYIUVBUVFUHWNUVLYJUUTUVAUVFWQZUVJUVCUVDUVEWRZU + VCUVDUVEWSZWTYJOUUDUTUVBUVFUUPVIZUVGDEFNPRXHXPUVLUVJAUUSXFYIUVBUVFULWNZ + WHUVGGMUSRXKYBAYKXFYIUVBUVFUIWNZUVHUVKUEUGWIWJUVGGMTXTXSRXKYAYBUEUGUPYJ + MVNVGUVBUVFYJMYLXAVIUVHUVGFGXONUVIUVMWPZUVKUVGUQURFUSNOPRXNXHXOUVLUVMUV + NUVPUVGDEFNPRXHXOUVLUVMUVQWHUVGGMUSRXKYAUVRUVHUVSUEUGWIWJUVGUQURFUSNOPR + XMXOXPUVMUVJUVOUVPUVGDEFNPRXOXPUVMUVJUVQWHUVGGMUSRYAYBUVRUVSUVKUEUGWIWJ + WTUEUGUVRXBXCXCXDXE $. + $} + + $d F a b c f g $. $d F c u v w z $. $d F u v x y $. $d G a b c f g $. + $d G c u v $. $d H a b c f g $. $d H c u v w z $. $d H u v x y $. + $d J a b c w z $. $d J c u v w z $. $d J u v x y $. $d K a b c f g $. + $d K c u v $. $d B a b c f g $. $d B c u v w z $. $d B u v x y $. + $d D a b c f g $. $d E a b c f g $. $d a b c f g ph $. $d ph u v $. + $( A functor to a thin category is determined entirely by the object part. + The hypothesis "functhinc.1" is related to a monotone function if + preorders induced by the categories are considered ( ~ catprs2 ). + (Contributed by Zhi Wang, 1-Oct-2024.) $) + functhinc $p |- ( ph -> ( F ( D Func E ) G <-> G = K ) ) $= + ( va vg vf vb vc vv vu cfunc co wbr wceq cv ccid cfv cop cco wral wa c1st + cxp c2nd cmap cixp wcel wf w3a eqid thinccd isfunc 3anass bitrdi mpbirand + cvv wfn funcf2lem simprl simprr adantr functhinclem2 functhinclem1 syl5bb + c0 wi anbi1d bitrd functhinclem4 mpbiran3d ) AJKHIUKULUMZKNUNZUDUOZHUPUQZ + UQWMWMKULUQWMJUQZIUPUQZUQUNUEUOZUFUOZWMUGUOZURUHUOZHUSUQZULULWMWTKULUQWQW + SWTKULUQWRWMWSKULUQWOWSJUQURWTJUQIUSUQZULULUNUEWSWTLULUTUFWMWSLULUTUHFUTU + GFUTVAUDFUTZAWKKUHFFVCZWTVBUQJUQWTVDUQJUQMULWTLUQVEULVFVGZXCVAZWLXCVAAWKF + GJVHZXFUAAWKXGXEXCVIXGXFVAAUDUGUHFGHXAWNUFUEIJKLWPMXBOPQRWNVJZWPVJZXAVJZX + BVJZSAITVKVLXGXEXCVMVNVOAXEWLXCXEKVPVGKXDVQUIUOZUJUOZLULXLJUQXMJUQMULXLXM + KULVHUJFUTUIFUTVIAWLUIUJUHFJKLMVRABCUIUJFGHIJKLMNOPQRTUAUBAXLFVGZXMFVGZVA + ZVADEFJLMXLXMAXNXOVSAXNXOVTADUOZJUQEUOZJUQMULWEUNXQXRLULWEUNWFEFUTDFUTXPU + CWAWBWCWDWGWHABCDEFGHXAWNUFUEIJKLWPMNXBUDUGUHOPQRSTUAUBUCXHXIXJXKWIWJ $. + $} + + ${ + $d B f x y $. $d C f x y $. $d D f x y $. $d F f x y $. $d G f x y $. + $d H f x y $. $d J f x y $. $d X x y $. $d Y x y $. + fullthinc.b $e |- B = ( Base ` C ) $. + fullthinc.j $e |- J = ( Hom ` D ) $. + fullthinc.h $e |- H = ( Hom ` C ) $. + fullthinc.d $e |- ( ph -> D e. ThinCat ) $. + ${ + fullthinc.f $e |- ( ph -> F ( C Func D ) G ) $. + $( A functor to a thin category is full iff empty hom-sets are mapped to + empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.) $) + fullthinc $p |- ( ph -> ( F ( C Full D ) G + <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> + ( ( F ` x ) J ( F ` y ) ) = (/) ) ) ) $= + ( vf co c0 wceq wa cthinc wcel cfunc wbr cful cv cfv wi wral wb isfull2 + foeq2 fo00 simprbi syl6bi com12 2ralimi simplbiim adantl simplr wn imor + wfo wo csn wex wne weu simprl simprr funcf2 adantr simpr neqned fdomne0 + wf syl2anc simprd cbs simplll eqid funcf1 ffvelrnd eqidd chom thincn0eu + a1i mpbid eusn sylib simpld foconst anbi1d foeq3 imbi12d mpbiri exlimiv + feq3 imp syl12anc f00 biimpri syl5ibr jaodan sylan2b ralimdvva sylanbrc + ex impbida ) AFUAUBZGHEFUCQUDZGHEFUEQUDZBUFZCUFZIQZRSZXMGUGZXNGUGZJQZRS + ZUHZCDUIBDUIZUJNOXJXKTZXLYBXLYBYCXLXKXOXSXMXNHQZVCZCDUIBDUIZYBBCDEFGHIJ + KLMUKZYEYABCDDXPYEXTXPYERXSYDVCZXTXORXSYDULZYHYDRSZXTXSYDUMZUNUOUPUQURU + SYCYBTXKYFXLXJXKYBUTYCYBYFYCYAYEBCDDYCXMDUBZXNDUBZTZTZYAYEYAYOXPVAZXTVD + YEXPXTVBYOYPYEXTYOYPTZXSPUFZVEZSZPVFZXOXSYDVPZYDRVGZYEYQYRXSUBPVHZUUAYQ + XSRVGZUUDYQUUCUUEYQUUBXORVGUUCUUETYOUUBYPYODEFGHIJXMXNKMLXJXKYNUTZYCYLY + MVIZYCYLYMVJZVKZVLZYQXORYOYPVMVNYDXOXSVOVQZVRYQFVSUGZFPJXQXRXJXKYNYPVTY + QDUULXMGYQDUULEFGHKUULWAYOXKYPUUFVLWBZYOYLYPUUGVLWCYQDUULXNGUUMYOYMYPUU + HVLWCYQUULWDJFWEUGSYQLWGWFWHPXSWIWJUUJYQUUCUUEUUKWKUUAUUBUUCTZYEYTUUNYE + UHZPYTUUOXOYSYDVPZUUCTZXOYSYDVCZUHXOYRYDWLYTUUNUUQYEUURYTUUBUUPUUCXSYSX + OYDWRWMXSYSXOYDWNWOWPWQWSWTYOXTTZXPYJXTYEUUSYJXPUUSXORYDVPZYJXPTUUSUUBU + UTYOUUBXTUUIVLXTUUBUUTUJYOXSRXOYDWRUSWHXOYDXAWJZVRUUSYJXPUVAWKYOXTVMXPY + JXTTZYEUVBYEXPYHYHUVBYKXBYIXCWSWTXDXEXHXFWSYGXGXIVQ $. + $} + + ${ + fullthinc2.f $e |- ( ph -> F ( C Full D ) G ) $. + fullthinc2.x $e |- ( ph -> X e. B ) $. + fullthinc2.y $e |- ( ph -> Y e. B ) $. + $( A full functor to a thin category maps empty hom-sets to empty + hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.) $) + fullthinc2 $p |- ( ph -> ( ( X H Y ) = (/) <-> + ( ( F ` X ) J ( F ` Y ) ) = (/) ) ) $= + ( co c0 wceq vx vy cfv wcel cv wral cful cfunc fullfunc ssbri fullthinc + wi wbr syl mpbid oveq12 eqeq1d simpl fveq2d oveq12d imbi12d rspc2gv imp + wa simpr syl21anc funcf2 f002 impbid ) AIJGRZSTZIEUCZJEUCZHRZSTZAIBUDZJ + BUDZUAUEZUBUEZGRZSTZVREUCZVSEUCZHRZSTZULZUBBUFUABUFZVKVOULZPQAEFCDUGRZU + MZWGOAUAUBBCDEFGHKLMNAWJEFCDUHRZUMOWIWKEFCDUIUJUNZUKUOVPVQVDWGWHWFWHUAU + BIJBBVRITZVSJTZVDZWAVKWEVOWOVTVJSVRIVSJGUPUQWOWDVNSWOWBVLWCVMHWOVRIEWMW + NURUSWOVSJEWMWNVEUSUTUQVAVBVCVFAVJVNIJFRABCDEFGHIJKMLWLPQVGVHVI $. + $} + $} + + ${ + $d B f x y $. $d C f x y $. $d D f x y $. $d F f x y $. $d G f x y $. + $d H f x y $. $d J f x y $. $d f ph x y $. + thincfth.b $e |- B = ( Base ` C ) $. + thincfth.h $e |- H = ( Hom ` C ) $. + thincfth.j $e |- J = ( Hom ` D ) $. + thincfth.c $e |- ( ph -> C e. ThinCat ) $. + thincfth.f $e |- ( ph -> F ( C Func D ) G ) $. + $( A functor from a thin category is faithful. (Contributed by Zhi Wang, + 1-Oct-2024.) $) + thincfth $p |- ( ph -> F ( C Faith D ) G ) $= + ( vx vy vf co wbr cv wcel cfunc cfv wf1 wral cfth wa wmo wf cthinc adantr + simprl simprr thincmo funcf2 f1mo syl2anc ralrimivva isfth2 sylanbrc ) AE + FCDUAQRZNSZOSZGQZVAEUBVBEUBHQZVAVBFQZUCZOBUDNBUDEFCDUEQRMAVFNOBBAVABTZVBB + TZUFZUFZPSVCTPUGVCVDVEUHVFVJBCPGVAVBACUITVILUJAVGVHUKZAVGVHULZIJUMVJBCDEF + GHVAVBIJKAUTVIMUJVKVLUNPVCVDVEUOUPUQNOBCDEFGHIJKURUS $. + $} ${ $d C f x y $. @@ -780084,6 +781274,75 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence VDRSVEUTURVDRUEUFUGUHUSVHBCURUIULUJUKUMUNMUOUP $. $} + ${ + thincsect.c $e |- ( ph -> C e. ThinCat ) $. + thincsect.b $e |- B = ( Base ` C ) $. + thincsect.x $e |- ( ph -> X e. B ) $. + thincsect.y $e |- ( ph -> Y e. B ) $. + ${ + thincsect.s $e |- S = ( Sect ` C ) $. + ${ + thincsect.h $e |- H = ( Hom ` C ) $. + $( In a thin category, one morphism is a section of another iff they + are pointing towards each other. (Contributed by Zhi Wang, + 24-Sep-2024.) $) + thincsect $p |- ( ph -> ( F ( X S Y ) G + <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) ) $= + ( co wcel wa cfv adantr wbr cop cco ccid wceq w3a eqid thinccd issect + df-3an bitrdi cthinc ccat simprl simprr catcocl thincid mpbiran3d ) A + EFHIDPUAZEHIGPQZFIHGPQZRZFEHIUBHCUCSZPPZHCUDSZSUEZAUSUTVAVFUFVBVFRABC + DVCVEEFGHIKOVCUGZVEUGZNACJUHZLMUIUTVAVFUJUKAVBRZBCVEVDGHACULQVBJTKOAH + BQVBLTZVHVJBCVCEFGHIHKOVGACUMQVBVITVKAIBQVBMTVKAUTVAUNAUTVAUOUPUQUR + $. + $} + + $( In a thin category, ` F ` is a section of ` G ` iff ` G ` is a section + of ` F ` . (Contributed by Zhi Wang, 24-Sep-2024.) $) + thincsect2 $p |- ( ph -> ( F ( X S Y ) G <-> G ( Y S X ) F ) ) $= + ( chom cfv co wcel wa wbr thincsect wb ancom a1i eqid 3bitr4d ) AEGHCNO + ZPQZFHGUFPQZRZUHUGRZEFGHDPSFEHGDPSUIUJUAAUGUHUBUCABCDEFUFGHIJKLMUFUDZTA + BCDFEUFHGIJLKMUKTUE $. + + thincinv.n $e |- N = ( Inv ` C ) $. + $( In a thin category, ` F ` is an inverse of ` G ` iff ` F ` is a + section of ` G ` (Contributed by Zhi Wang, 24-Sep-2024.) $) + thincinv $p |- ( ph -> ( F ( X N Y ) G <-> F ( X S Y ) G ) ) $= + ( co wbr thinccd isinv thincsect2 biimpa mpbiran3d ) AEFHIGPQEFHIDPQZFE + IHDPQZABCDEFGHIKOACJRLMNSAUCUDABCDEFHIJKLMNTUAUB $. + $} + + $d C f g $. $d F f g $. $d H f g $. $d I f g $. $d X f g $. + $d Y f g $. $d f g ph $. + thinciso.h $e |- H = ( Hom ` C ) $. + ${ + thinciso.i $e |- I = ( Iso ` C ) $. + thinciso.f $e |- ( ph -> F e. ( X H Y ) ) $. + $( In a thin category, ` F : X --> Y ` is an isomorphism iff there is a + morphism from ` Y ` to ` X ` . (Contributed by Zhi Wang, + 25-Sep-2024.) $) + thinciso $p |- ( ph -> ( F e. ( X I Y ) <-> ( Y H X ) =/= (/) ) ) $= + ( vg co wcel wa wtru cv csect cfv wbr wrex c0 wne thinccd dfiso3 simprl + eqid ad2antrr cthinc thincsect mpbir2and trud reximdva0 reximddv adantl + jca rexn0 impbida bitr4d ) ADGHFQRPUAZDHGCUBUCZQUDZDVDGHVEQUDZSZPHGEQZU + EZVIUFUGZABCVEPDEFGHJMNVEUKZACIUHKLOUIAVKVJAVKSZTVHPVIVMVDVIRZTSZSZVFVG + VPVFVNDGHEQRZVMVNTUJZAVQVKVOOULZVPBCVEVDDEHGACUMRVKVOIULZJAHBRVKVOLULZA + GBRVKVOKULZVLMUNUOVPVGVQVNVSVRVPBCVEDVDEGHVTJWBWAVLMUNUOUTATPVIAVNSUPUQ + URVJVKAVHPVIVAUSVBVC $. + $} + + $( In a thin category, two objects are isomorphic iff there are morphisms + between them in both directions. (Contributed by Zhi Wang, + 25-Sep-2024.) $) + thinccic $p |- ( ph -> ( X ( ~=c ` C ) Y <-> + ( ( X H Y ) =/= (/) /\ ( Y H X ) =/= (/) ) ) ) $= + ( vf cfv co wcel wex c0 wne wa adantr cv ciso ccic wbr eqid isohom sselda + thinccd cthinc simpr thinciso biadanid exbidv cic wb anbi1i 19.41v bitr4i + n0 a1i 3bitr4d ) ALUAZEFCUBMZNZOZLPVBEFDNZOZFEDNQRZSZLPZEFCUCMUDVFQRZVHSZ + AVEVILAVEVGVHAVDVFVBABCDVCEFHKVCUEZACGUHZIJUFUGAVGSBCVBDVCEFACUIOVGGTHAEB + OVGITAFBOVGJTKVMAVGUJUKULUMABCLVCEFVMHVNIJUNVLVJUOAVLVGLPZVHSVJVKVOVHLVFU + SUPVGVHLUQURUTVA $. + $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -780268,6 +781527,46 @@ mean the category of preordered sets (classes). However, "ProsetToCat" $} $} + ${ + $d B x y $. $d C x y $. $d ph x y $. + postc.c $e |- ( ph -> C = ( ProsetToCat ` K ) ) $. + postc.k $e |- ( ph -> K e. Proset ) $. + ${ + $d K x y $. + $( The converted category is a poset iff the original proset is a poset. + (Contributed by Zhi Wang, 26-Sep-2024.) $) + postcpos $p |- ( ph -> ( K e. Poset <-> C e. Poset ) ) $= + ( vx vy cbs cfv cproset prstcprs eqidd prstcbas cv cple wb wcel prstcle + wbr wa adantr pospropd ) AFGCHIZCBJJEABCDEKAUCLZAUCBCDEUDMAFNZGNZCOIZSU + EUFBOISPUEUCQUFUCQTABCUGUEUFDEAUGLRUAUB $. + + $( Alternate proof for ~ postcpos . (Contributed by Zhi Wang, + 25-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + postcposALT $p |- ( ph -> ( K e. Poset <-> C e. Poset ) ) $= + ( vx vy cv cple cfv wbr wa wi cbs wral cpo wcel eqidd prstcle eqid baib + weq prstcbas anbi12d imbi1d raleqbidvv cproset ispos2 prstcprs 3bitr4d + wb syl ) AFHZGHZCIJZKZUNUMUOKZLZFGUBZMZGCNJZOZFVAOZUMUNBIJZKZUNUMVDKZLZ + USMZGBNJZOZFVIOZCPQZBPQZAVBVJFVAVIAVABCDEAVARUCZAUTVHGVAVIVNAURVGUSAUPV + EUQVFABCUOUMUNDEAUORZSABCUOUNUMDEVOSUDUEUFUFACUGQZVLVCUKEVLVPVCFGVACUOV + ATUOTUHUAULABUGQZVMVKUKABCDEUIVMVQVKFGVIBVDVITVDTUHUAULUJ $. + $} + + postc.b $e |- B = ( Base ` C ) $. + $( The converted category is a poset iff no distinct objects are + isomorphic. (Contributed by Zhi Wang, 25-Sep-2024.) $) + postc $p |- ( ph -> ( C e. Poset <-> A. x e. B A. y e. B + ( x ( ~=c ` C ) y -> x = y ) ) ) $= + ( wcel cv cfv wbr wa wceq wi wral cproset eqid co cpo cple ccic wb ispos2 + prstcprs baib syl chom wne cprstc adantr prstcthin simprl simprr thinccic + c0 eqidd cbs eleqtrdi prstchom anbi12d bitr4d imbi1d 2ralbidva ) AEUAJZBK + ZCKZEUBLZMZVHVGVIMZNZVGVHOZPZCDQBDQZVGVHEUCLMZVMPZCDQBDQAERJZVFVOUDAEFGHU + FVFVRVOBCDEVIIVISUEUGUHAVQVNBCDDAVGDJZVHDJZNZNZVPVLVMWBVPVGVHEUILZTUQUJZV + HVGWCTUQUJZNVLWBDEWCVGVHWBEFAEFUKLOWAGULZAFRJWAHULZUMIAVSVTUNZAVSVTUOZWCS + UPWBVJWDVKWEWBEWCFVIVGVHWFWGWBVIURZWBWCURZWBVGDEUSLZWHIUTZWBVHDWLWIIUTZVA + WBEWCFVIVHVGWFWGWJWKWNWMVAVBVCVDVEVC $. + $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -780281,7 +781580,7 @@ mean the category of preordered sets (classes). However, "ProsetToCat" cmndtc $a class MndToCat $. ${ - $d B x $. $d M m x $. $d m ph $. + $d B x y $. $d M m x $. $d X x y $. $d Y x y $. $d m ph $. $( Definition of the function converting a monoid to a category. Example 3.3(4.e) of [Adamek] p. 24. @@ -780338,6 +781637,13 @@ structure becomes the object here (see ~ mndtcbasval ) , instead of just ABCDFGHMNAEBKTUAOIEDBPQR $. mndtchom.y $e |- ( ph -> Y e. B ) $. + $( Two objects in a category built from a monoid are identical. + (Contributed by Zhi Wang, 24-Sep-2024.) $) + mndtcbas2 $p |- ( ph -> X = Y ) $= + ( vx vy cv wceq wral wcel weu wmo mndtcbas eumo moel 3syl rspc2gv syl2anc + biimpi wi eqeq12 mpd ) ALNZMNZOZMBPLBPZEFOZAUJBQZLRUOLSZUMALBCDGHITUOLUAU + PUMLMBUBUFUCAEBQFBQUMUNUGJKULUNLMEFBBUJEUKFUHUDUEUI $. + ${ mndtchom.h $e |- ( ph -> H = ( Hom ` C ) ) $. $( The only hom-set of the category built from a monoid is the base set @@ -780439,7 +781745,7 @@ structure becomes the object here (see ~ mndtcbasval ) , instead of just ( cfv co wcel eqid ad2antrr vf vg vz vh cmon chom cop cco wceq wral cbs cv wi grpmndd mndtccat eleqtrd ismon2 w3a cplusg cmndtc simpr1 eleqtrrd wa cmnd eqidd mndtcco2 eqeq12d wb simpr2 mndtchom simpr3 simplr grplcan - cgrp syl13anc bitrd biimpd ralrimivvva monepilem eqrdv oveqd 3eqtr4d ) + cgrp syl13anc bitrd biimpd ralrimivvva mpbiran3d eqrdv oveqd 3eqtr4d ) AGHCUEPZQZGHCUFPZQZGHFQGHEQAUAWDWFAUAULZWDRWGWFRZWGUBULZUCULZGUGHCUHPZQ ZQZWGUDULZWLQZUIZWIWNUIZUMZUDWJGWEQZUJUBWSUJUCCUKPZUJAUCWTCWKUBUDWGWEWC GHWTSWESWKSWCSACDIADJUNZUOAGBWTLKUPAHBWTMKUPUQAWHVCZWRUCUBUDWTWSWSXBWJW @@ -780459,7 +781765,7 @@ structure becomes the object here (see ~ mndtcbasval ) , instead of just ( cfv co wcel eqid ad2antrr vf vg vz vh cepi chom cop cco wceq wral cbs cv wi grpmndd mndtccat eleqtrd isepi2 w3a cplusg cmndtc simpr1 eleqtrrd wa cmnd eqidd mndtcco2 eqeq12d wb simpr2 mndtchom simpr3 simplr grprcan - cgrp syl13anc bitrd biimpd ralrimivvva monepilem eqrdv oveqd 3eqtr4d ) + cgrp syl13anc bitrd biimpd ralrimivvva mpbiran3d eqrdv oveqd 3eqtr4d ) AGHCUEPZQZGHCUFPZQZGHDQGHFQAUAWDWFAUAULZWDRWGWFRZUBULZWGGHUGUCULZCUHPZQ ZQZUDULZWGWLQZUIZWIWNUIZUMZUDHWJWEQZUJUBWSUJUCCUKPZUJAUCWTCWKUBUDWCWGWE GHWTSWESWKSWCSACEIAEJUNZUOAGBWTLKUPAHBWTMKUPUQAWHVCZWRUCUBUDWTWSWSXBWJW