From ff48fe13191e1dd28a9b533fc7a7d125d9b92f92 Mon Sep 17 00:00:00 2001 From: zwang123 Date: Tue, 24 Sep 2024 03:27:58 +0900 Subject: [PATCH] Added thin category and preordered sets (#4220) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Move moel to main; add ThinCat and indiscrete category * add thincc * Add catcone0 to main; add catprs, prsthinc and related theorems * remove ax-un dependency in f1omo * remove ax-un for 2oexw and prsthinc * remove ax-un and ax-pow for indthinc * shorten 2oexw * add mo0sn * add mofasn2 and related * add mofsn3 and rename theorems xxfa* -> xxf* * add setcthin and setc2othin * shorten proof by mof02 * rename mofsn3 -> mofmo; and fix description * Add ProsetToCat defining and important properties * added two redundant hypotheses to prstchom for explicitness * add prstchom2ALT * add thincn0eu and prstchom2 * revive ALT theorems * prevent basendx usage * shorten prstchomval * sylibda->sylbida * more info in description of df-prstc and df-thinc * 1oexw -> 1oex, 2oexw -> 2oex; og ones become OLD * remove empty chapter * fix description of eufsn eufsn2 mofsn; less axiom -> fewer axiom * fix description of mofsn2, mofmo, fvconst0ci, and fvconstdomi; rename fconst* -> fvconst*. * fix description for thincmo and thincmoALT; thincum -> thincmo2 * add rextru and reutru * add mosssn, mosssn2 * mof0w -> mof0ALT * Fixed descriptions based on BJ’s suggestion * set catprs2 as the main theorem * slightly change the description of catprs2 * add catprsc2 * add mofsssn --- changes-set.txt | 2 + discouraged | 28 ++ set.mm | 1150 ++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 1108 insertions(+), 72 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index e97a36e430..609bb44099 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -100,6 +100,8 @@ DONE: Date Old New Notes 21-Sep-24 sb56 sbalex substitution expressed with 'al' or with 'ex' 21-Sep-24 nanimn dfnan2 mark as an alternative definition +18-Sep-24 sylibda sylbida moved from SN's mathbox to main set.mm +17-Sep-24 moel [same] moved from TA's mathbox to main set.mm 16-Sep-24 syl5eqr eqtr3id compare to eqtr3i or eqtr3d 14-Sep-24 iunsn [same] moved from SN's mathbox to main set.mm 10-Sep-24 sspreima [same] moved from TA's mathbox to main set.mm diff --git a/discouraged b/discouraged index 6d3b805fdb..9e1535ba52 100644 --- a/discouraged +++ b/discouraged @@ -4923,6 +4923,7 @@ "df-pnf" is used by "mnfnre". "df-pnf" is used by "pnfex". "df-pnf" is used by "pnfnre". +"df-prstc" is used by "prstcval". "df-r" is used by "avril1". "df-r" is used by "ax1rid". "df-r" is used by "axresscn". @@ -12039,6 +12040,13 @@ "prpssnq" is used by "reclem2pr". "prpssnq" is used by "suplem1pr". "prpssnq" is used by "wuncn". +"prstchomval" is used by "prstchom". +"prstchomval" is used by "prstchom2ALT". +"prstchomval" is used by "prstcthin". +"prstcnidlem" is used by "prstchomval". +"prstcnidlem" is used by "prstcnid". +"prstcval" is used by "prstcnidlem". +"prstcval" is used by "prstcthin". "prub" is used by "genpnnp". "prub" is used by "ltexprlem6". "prub" is used by "ltexprlem7". @@ -13826,6 +13834,7 @@ New usage of "1lt2pi" is discouraged (1 uses). New usage of "1ne0sr" is discouraged (1 uses). New usage of "1nq" is discouraged (9 uses). New usage of "1nqenq" is discouraged (1 uses). +New usage of "1oexOLD" is discouraged (0 uses). New usage of "1p1e2apr1" is discouraged (0 uses). New usage of "1p2e3ALT" is discouraged (0 uses). New usage of "1pi" is discouraged (11 uses). @@ -13864,6 +13873,7 @@ New usage of "2lplnm2N" is discouraged (0 uses). New usage of "2lplnmN" is discouraged (0 uses). New usage of "2moex" is discouraged (2 uses). New usage of "2moswap" is discouraged (1 uses). +New usage of "2oexOLD" is discouraged (0 uses). New usage of "2pm13.193" is discouraged (3 uses). New usage of "2pm13.193VD" is discouraged (0 uses). New usage of "2pmaplubN" is discouraged (1 uses). @@ -15466,6 +15476,7 @@ New usage of "df-plpq" is discouraged (3 uses). New usage of "df-plq" is discouraged (2 uses). New usage of "df-plr" is discouraged (2 uses). New usage of "df-pnf" is discouraged (3 uses). +New usage of "df-prstc" is discouraged (1 uses). New usage of "df-r" is discouraged (6 uses). New usage of "df-ringcALTV" is discouraged (1 uses). New usage of "df-rngcALTV" is discouraged (1 uses). @@ -16095,6 +16106,7 @@ New usage of "expcomdg" is discouraged (0 uses). New usage of "f1cofveqaeqALT" is discouraged (0 uses). New usage of "f1dmOLD" is discouraged (0 uses). New usage of "f1eqcocnvOLD" is discouraged (0 uses). +New usage of "f1omoALT" is discouraged (0 uses). New usage of "f1oweALT" is discouraged (0 uses). New usage of "f1rhm0to0ALT" is discouraged (0 uses). New usage of "falnorfalOLD" is discouraged (0 uses). @@ -16742,6 +16754,7 @@ New usage of "indistps2ALT" is discouraged (0 uses). New usage of "indistpsALT" is discouraged (0 uses). New usage of "indistpsx" is discouraged (0 uses). New usage of "indpi" is discouraged (1 uses). +New usage of "indthincALT" is discouraged (0 uses). New usage of "infpssALT" is discouraged (0 uses). New usage of "int2" is discouraged (3 uses). New usage of "int3" is discouraged (1 uses). @@ -17233,6 +17246,7 @@ New usage of "mobidvALT" is discouraged (0 uses). New usage of "mobiiOLD" is discouraged (0 uses). New usage of "moexex" is discouraged (2 uses). New usage of "moexexv" is discouraged (0 uses). +New usage of "mof0ALT" is discouraged (0 uses). New usage of "mpjao3danOLD" is discouraged (0 uses). New usage of "mpofunOLD" is discouraged (0 uses). New usage of "mpteq12dvOLD" is discouraged (0 uses). @@ -17984,6 +17998,10 @@ New usage of "prnmadd" is discouraged (2 uses). New usage of "prnmax" is discouraged (7 uses). New usage of "probfinmeasbALTV" is discouraged (0 uses). New usage of "prpssnq" is discouraged (8 uses). +New usage of "prstchom2ALT" is discouraged (0 uses). +New usage of "prstchomval" is discouraged (3 uses). +New usage of "prstcnidlem" is discouraged (2 uses). +New usage of "prstcval" is discouraged (2 uses). New usage of "prub" is discouraged (6 uses). New usage of "psrass1lemOLD" is discouraged (0 uses). New usage of "psrbagaddclOLD" is discouraged (1 uses). @@ -18099,6 +18117,7 @@ New usage of "retbwax1" is discouraged (0 uses). New usage of "retbwax2" is discouraged (3 uses). New usage of "retbwax3" is discouraged (0 uses). New usage of "retbwax4" is discouraged (0 uses). +New usage of "reutruALT" is discouraged (0 uses). New usage of "rexab2OLD" is discouraged (0 uses). New usage of "rexbidvALT" is discouraged (0 uses). New usage of "rexbidvaALT" is discouraged (0 uses). @@ -18587,6 +18606,7 @@ New usage of "tendospcanN" is discouraged (1 uses). New usage of "tfr1ALT" is discouraged (0 uses). New usage of "tfr2ALT" is discouraged (0 uses). New usage of "tfr3ALT" is discouraged (0 uses). +New usage of "thincmoALT" is discouraged (0 uses). New usage of "topnfbey" is discouraged (0 uses). New usage of "tpid3gVD" is discouraged (0 uses). New usage of "tratrb" is discouraged (2 uses). @@ -18806,6 +18826,7 @@ Proof modification of "19.41rg" is discouraged (58 steps). Proof modification of "19.41rgVD" is discouraged (127 steps). Proof modification of "19.43OLD" is discouraged (72 steps). Proof modification of "1div0apr" is discouraged (77 steps). +Proof modification of "1oexOLD" is discouraged (4 steps). Proof modification of "1p1e2apr1" is discouraged (7 steps). Proof modification of "1p2e3ALT" is discouraged (7 steps). Proof modification of "1t1e1ALT" is discouraged (13 steps). @@ -18816,6 +18837,7 @@ Proof modification of "2eu5OLD" is discouraged (81 steps). Proof modification of "2falsedOLD" is discouraged (14 steps). Proof modification of "2irrexpqALT" is discouraged (90 steps). Proof modification of "2logb9irrALT" is discouraged (141 steps). +Proof modification of "2oexOLD" is discouraged (9 steps). Proof modification of "2pm13.193" is discouraged (91 steps). Proof modification of "2pm13.193VD" is discouraged (223 steps). Proof modification of "2sb5nd" is discouraged (125 steps). @@ -19566,6 +19588,7 @@ Proof modification of "exlimexi" is discouraged (15 steps). Proof modification of "f1cofveqaeqALT" is discouraged (124 steps). Proof modification of "f1dmOLD" is discouraged (19 steps). Proof modification of "f1eqcocnvOLD" is discouraged (361 steps). +Proof modification of "f1omoALT" is discouraged (39 steps). Proof modification of "f1oweALT" is discouraged (805 steps). Proof modification of "f1rhm0to0ALT" is discouraged (161 steps). Proof modification of "falimfal" is discouraged (6 steps). @@ -19843,6 +19866,7 @@ Proof modification of "incomOLD" is discouraged (37 steps). Proof modification of "indifdirOLD" is discouraged (147 steps). Proof modification of "indistps2ALT" is discouraged (43 steps). Proof modification of "indistpsALT" is discouraged (64 steps). +Proof modification of "indthincALT" is discouraged (202 steps). Proof modification of "infpssALT" is discouraged (52 steps). Proof modification of "infregelb" is discouraged (185 steps). Proof modification of "int2" is discouraged (14 steps). @@ -19941,6 +19965,7 @@ Proof modification of "mndoissmgrpOLD" is discouraged (22 steps). Proof modification of "mo4OLD" is discouraged (9 steps). Proof modification of "mobidvALT" is discouraged (48 steps). Proof modification of "mobiiOLD" is discouraged (17 steps). +Proof modification of "mof0ALT" is discouraged (67 steps). Proof modification of "mpjao3danOLD" is discouraged (29 steps). Proof modification of "mpofunOLD" is discouraged (95 steps). Proof modification of "mpteq12dvOLD" is discouraged (18 steps). @@ -20067,6 +20092,7 @@ Proof modification of "problem2" is discouraged (104 steps). Proof modification of "problem3" is discouraged (56 steps). Proof modification of "problem4" is discouraged (310 steps). Proof modification of "problem5" is discouraged (133 steps). +Proof modification of "prstchom2ALT" is discouraged (121 steps). Proof modification of "psrass1lemOLD" is discouraged (1513 steps). Proof modification of "psrbagaddclOLD" is discouraged (392 steps). Proof modification of "psrbagconOLD" is discouraged (365 steps). @@ -20141,6 +20167,7 @@ Proof modification of "retbwax1" is discouraged (195 steps). Proof modification of "retbwax2" is discouraged (127 steps). Proof modification of "retbwax3" is discouraged (20 steps). Proof modification of "retbwax4" is discouraged (13 steps). +Proof modification of "reutruALT" is discouraged (45 steps). Proof modification of "rexab2OLD" is discouraged (67 steps). Proof modification of "rexbidvALT" is discouraged (10 steps). Proof modification of "rexbidvaALT" is discouraged (10 steps). @@ -20292,6 +20319,7 @@ Proof modification of "tdeglem4OLD" is discouraged (703 steps). Proof modification of "tfr1ALT" is discouraged (19 steps). Proof modification of "tfr2ALT" is discouraged (52 steps). Proof modification of "tfr3ALT" is discouraged (84 steps). +Proof modification of "thincmoALT" is discouraged (93 steps). Proof modification of "topnfbey" is discouraged (75 steps). Proof modification of "toycom" is discouraged (142 steps). Proof modification of "tpid3gVD" is discouraged (116 steps). diff --git a/set.mm b/set.mm index cfbc10e025..a1d6520057 100644 --- a/set.mm +++ b/set.mm @@ -5467,6 +5467,14 @@ use disjunction (although this is not required since definitions are ( wa simpl syl2anc ) ABGACDABHEFI $. $} + ${ + sylbida.1 $e |- ( ph -> ( ps <-> ch ) ) $. + sylbida.2 $e |- ( ( ph /\ ch ) -> th ) $. + $( A syllogism deduction. (Contributed by SN, 16-Jul-2024.) $) + sylbida $p |- ( ( ph /\ ps ) -> th ) $= + ( biimpa syldan ) ABCDABCEGFH $. + $} + ${ sylan2.1 $e |- ( ph -> ch ) $. sylan2.2 $e |- ( ( ps /\ ch ) -> th ) $. @@ -30671,6 +30679,17 @@ generally appear in a single form (either definitional, but more often K $. $} + ${ + $d x y A $. + $( "At most one" element in a set. (Contributed by Thierry Arnoux, + 26-Jul-2018.) $) + moel $p |- ( E* x x e. A <-> A. x e. A A. y e. A x = y ) $= + ( cv wcel weq wi wal wmo ralcom4 df-ral ralbii wa alcom eleq1w mo4 impexp + wral albii bitr4i 3bitr4i 3bitr4ri ) BDCEZABFZGZBHZACRUEACRZBHZUDBCRZACRA + DCEZAIZUEABCJUIUFACUDBCKLUJUCMUDGZBHAHULAHZBHUKUHULABNUJUCABABCOPUGUMBUGU + JUEGZAHUMUEACKULUNAUJUCUDQSTSUAUB $. + $} + $( Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.) $) mormo $p |- ( E* x ph -> E* x e. A ph ) $= @@ -81047,20 +81066,11 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and 1on $p |- 1o e. On $= ( c1o c0 csuc con0 df-1o 0elon onsuci eqeltri ) ABCDEBFGH $. - $( Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by - AV, 1-Jul-2022.) $) - 1oex $p |- 1o e. _V $= - ( c1o con0 1on elexi ) ABCD $. - $( Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) $) 2on $p |- 2o e. On $= ( c2o c1o csuc con0 df-2o 1on onsuci eqeltri ) ABCDEBFGH $. - $( ` 2o ` is a set. (Contributed by BJ, 6-Apr-2019.) $) - 2oex $p |- 2o e. _V $= - ( c2o c1o csuc cvv df-2o 1oex sucex eqeltri ) ABCDEBFGH $. - $( Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) $) 2on0 $p |- 2o =/= (/) $= ( c2o c1o csuc c0 df-2o nsuceq0 eqnetri ) ABCDEBFG $. @@ -81080,6 +81090,19 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and df1o2 $p |- 1o = { (/) } $= ( c1o c0 csuc csn df-1o suc0 eqtri ) ABCBDEFG $. + $( Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by + AV, 1-Jul-2022.) Remove dependency on ~ ax-10 , ~ ax-11 , ~ ax-12 , + ~ ax-un . (Revised by Zhi Wang, 19-Sep-2024.) $) + 1oex $p |- 1o e. _V $= + ( c1o c0 csn cvv df1o2 snex eqeltri ) ABCDEBFG $. + $( $j usage '1oex' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-un'; $) + + $( Obsolete version of ~ 1oex as of 19-Sep-2024. (Contributed by BJ, + 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + 1oexOLD $p |- 1o e. _V $= + ( c1o con0 1on elexi ) ABCD $. + $( Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) $) df2o3 $p |- 2o = { (/) , 1o } $= @@ -81091,6 +81114,19 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and df2o2 $p |- 2o = { (/) , { (/) } } $= ( c2o c0 c1o cpr csn df2o3 df1o2 preq2i eqtri ) ABCDBBEZDFCJBGHI $. + $( ` 2o ` is a set. (Contributed by BJ, 6-Apr-2019.) Remove dependency on + ~ ax-10 , ~ ax-11 , ~ ax-12 , ~ ax-un . (Proof shortened by Zhi Wang, + 19-Sep-2024.) $) + 2oex $p |- 2o e. _V $= + ( c2o c0 c1o cpr cvv df2o3 prex eqeltri ) ABCDEFBCGH $. + $( $j usage '2oex' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-un'; $) + + $( Obsolete version of ~ 2oex as of 19-Sep-2024. (Contributed by BJ, + 6-Apr-2019.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + 2oexOLD $p |- 2o e. _V $= + ( c2o c1o csuc cvv df-2o 1oex sucex eqeltri ) ABCDEBFGH $. + $( Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) $) 1n0 $p |- 1o =/= (/) $= @@ -202911,51 +202947,66 @@ concepts associated with those structures (product, substructure...) catcocl.x $e |- ( ph -> X e. B ) $. catcocl.y $e |- ( ph -> Y e. B ) $. catcocl.z $e |- ( ph -> Z e. B ) $. - catcocl.f $e |- ( ph -> F e. ( X H Y ) ) $. - catcocl.g $e |- ( ph -> G e. ( Y H Z ) ) $. - $( Closure of a composition arrow. (Contributed by Mario Carneiro, - 2-Jan-2017.) $) - catcocl $p |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) $= - ( co vg vf vx vy vz vv vw cv cop wcel wral ccat wceq wrex iscat ibi simpl - wa 2ralimi adantl ralimi adantr ad2antrr ad3antrrr simpllr simplr oveq12d - 3syl eleqtrrd simpr simp-5r simp-4r opeq12d oveq123d eleq12d rspcimdv mpd - rspcdv ) AUAUHZUBUHZUCUHZUDUHZUIZUEUHZDTZTZWAWDGTZUJZUAWBWDGTZUKZUBWAWBGT - ZUKZUEBUKZUDBUKZUCBUKZFEHIUIZJDTZTZHJGTZUJZACULUJZVSVTWBWAUIWADTTVTUMUBWB - WAGTUKVTVSWAWAUIWBDTTVTUMUBWKUKURUDBUKUAWAWAGTUNZWHUFUHZVSWBWDUIUGUHZDTTV - TWCXDDTTXCWFWAWDUIXDDTTUMUFWDXDGTUKUGBUKZURZUAWIUKUBWKUKZUEBUKUDBUKZURZUC - BUKZWONXAXJUCUDUEUGBCDUBUAUFGULKLMUOUPXIWNUCBXHWNXBXGWLUDUEBBXFWHUBUAWKWI - WHXEUQUSUSUTVAVHAWNWTUCHBOAWAHUMZURZWMWTUDIBAIBUJXKPVBXLWBIUMZURZWLWTUEJB - AJBUJXKXMQVCXNWDJUMZURZWJWTUBEWKXPEHIGTZWKAEXQUJXKXMXORVDXPWAHWBIGAXKXMXO - VEXLXMXOVFZVGVIXPVTEUMZURZWHWTUAFWIXPFWIUJXSXPFIJGTZWIAFYAUJXKXMXOSVDXPWB - IWDJGXRXNXOVJVGVIVBXTVSFUMZURZWFWRWGWSYCVSFVTEWEWQYCWCWPWDJDYCWAHWBIAXKXM - XOXSYBVKZXLXMXOXSYBVLVMXNXOXSYBVEZVGXTYBVJXPXSYBVFVNYCWAHWDJGYDYEVGVOVRVP - VPVPVPVQ $. - - catass.w $e |- ( ph -> W e. B ) $. - catass.g $e |- ( ph -> K e. ( Z H W ) ) $. - $( Associativity of composition in a category. (Contributed by Mario - Carneiro, 2-Jan-2017.) $) - catass $p |- ( ph -> + ${ + catcocl.f $e |- ( ph -> F e. ( X H Y ) ) $. + catcocl.g $e |- ( ph -> G e. ( Y H Z ) ) $. + $( Closure of a composition arrow. (Contributed by Mario Carneiro, + 2-Jan-2017.) $) + catcocl $p |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) $= + ( co vg vf vx vy vz vv vw cv cop wcel wral ccat wceq wa iscat ibi simpl + wrex 2ralimi adantl ralimi 3syl adantr ad3antrrr simpllr simplr oveq12d + ad2antrr eleqtrrd simpr simp-5r simp-4r opeq12d oveq123d eleq12d rspcdv + rspcimdv mpd ) AUAUHZUBUHZUCUHZUDUHZUIZUEUHZDTZTZWAWDGTZUJZUAWBWDGTZUKZ + UBWAWBGTZUKZUEBUKZUDBUKZUCBUKZFEHIUIZJDTZTZHJGTZUJZACULUJZVSVTWBWAUIWAD + TTVTUMUBWBWAGTUKVTVSWAWAUIWBDTTVTUMUBWKUKUNUDBUKUAWAWAGTURZWHUFUHZVSWBW + DUIUGUHZDTTVTWCXDDTTXCWFWAWDUIXDDTTUMUFWDXDGTUKUGBUKZUNZUAWIUKUBWKUKZUE + BUKUDBUKZUNZUCBUKZWONXAXJUCUDUEUGBCDUBUAUFGULKLMUOUPXIWNUCBXHWNXBXGWLUD + UEBBXFWHUBUAWKWIWHXEUQUSUSUTVAVBAWNWTUCHBOAWAHUMZUNZWMWTUDIBAIBUJXKPVCX + LWBIUMZUNZWLWTUEJBAJBUJXKXMQVHXNWDJUMZUNZWJWTUBEWKXPEHIGTZWKAEXQUJXKXMX + ORVDXPWAHWBIGAXKXMXOVEXLXMXOVFZVGVIXPVTEUMZUNZWHWTUAFWIXPFWIUJXSXPFIJGT + ZWIAFYAUJXKXMXOSVDXPWBIWDJGXRXNXOVJVGVIVCXTVSFUMZUNZWFWRWGWSYCVSFVTEWEW + QYCWCWPWDJDYCWAHWBIAXKXMXOXSYBVKZXLXMXOXSYBVLVMXNXOXSYBVEZVGXTYBVJXPXSY + BVFVNYCWAHWDJGYDYEVGVOVPVQVQVQVQVR $. + + catass.w $e |- ( ph -> W e. B ) $. + catass.g $e |- ( ph -> K e. ( Z H W ) ) $. + $( Associativity of composition in a category. (Contributed by Mario + Carneiro, 2-Jan-2017.) $) + catass $p |- ( ph -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) $= - ( vg vf vy vx vz vk vw cv cop co wceq wral wa wrex wcel ccat iscat adantr - ibi syl ad2antrr ad3antrrr simpllr simplr oveq12d ad4antr ad5antr ad6antr - eleqtrrd simp-4r simp-7r simp-6r opeq12d simp-5r oveq123d rspcdv rspcimdv - simpr eqeq12d adantld mpd ) AUDUKZUEUKZUFUKZUGUKZULWHDUMUMWFUNUEWGWHGUMUO - WFWEWHWHULWGDUMUMWFUNUEWHWGGUMZUOUPUFBUOUDWHWHGUMUQZWEWFWHWGULZUHUKZDUMZU - MZWHWLGUMURZUIUKZWEWGWLULZUJUKZDUMZUMZWFWKWRDUMZUMZWPWNWHWLULZWRDUMZUMZUN - ZUIWLWRGUMZUOZUJBUOZUPZUDWGWLGUMZUOZUEWIUOZUHBUOZUFBUOZUPZUGBUOZHFKLULZID - UMZUMZEJKULZIDUMZUMZHFEYALDUMZUMZJLULZIDUMZUMZUNZACUSURZXQPYJXQUGUFUHUJBC - DUEUDUIGUSMNOUTVBVCAXPYIUGJBQAWHJUNZUPZXOYIWJYLXNYIUFKBAKBURYKRVAYLWGKUNZ - UPZXMYIUHLBALBURYKYMSVDYNWLLUNZUPZXLYIUEEWIYPEJKGUMZWIAEYQURYKYMYOTVEYPWH - JWGKGAYKYMYOVFYLYMYOVGVHVLYPWFEUNZUPZXJYIUDFXKYSFKLGUMZXKAFYTURYKYMYOYRUA - VIYSWGKWLLGYLYMYOYRVFYNYOYRVGVHVLYSWEFUNZUPZXIYIWOUUBXHYIUJIBAIBURYKYMYOY - RUUAUBVJUUBWRIUNZUPZXFYIUIHXGUUDHLIGUMZXGAHUUEURYKYMYOYRUUAUUCUCVKUUDWLLW - RIGYNYOYRUUAUUCVMUUBUUCWAVHVLUUDWPHUNZUPZXBYCXEYHUUGWTXTWFEXAYBUUGWKYAWRI - DUUGWHJWGKAYKYMYOYRUUAUUCUUFVNZYLYMYOYRUUAUUCUUFVOZVPZUUBUUCUUFVGZVHUUGWP - HWEFWSXSUUGWQXRWRIDUUGWGKWLLUUIYNYOYRUUAUUCUUFVQZVPUUKVHUUDUUFWAZYSUUAUUC - UUFVFZVRYPYRUUAUUCUUFVMZVRUUGWPHWNYEXDYGUUGXCYFWRIDUUGWHJWLLUUHUULVPUUKVH - UUMUUGWEFWFEWMYDUUGWKYAWLLDUUJUULVHUUNUUOVRVRWBVSVTWCVTVTVTVTWCVTWD $. + ( vg vf vy vx vz vk vw cv cop co wceq wral wrex wcel ccat iscat ibi syl + adantr ad2antrr simpllr simplr oveq12d eleqtrrd ad4antr ad5antr ad6antr + ad3antrrr simp-4r simpr simp-7r simp-6r opeq12d simp-5r oveq123d rspcdv + wa eqeq12d rspcimdv adantld mpd ) AUDUKZUEUKZUFUKZUGUKZULWHDUMUMWFUNUEW + GWHGUMUOWFWEWHWHULWGDUMUMWFUNUEWHWGGUMZUOVTUFBUOUDWHWHGUMUPZWEWFWHWGULZ + UHUKZDUMZUMZWHWLGUMUQZUIUKZWEWGWLULZUJUKZDUMZUMZWFWKWRDUMZUMZWPWNWHWLUL + ZWRDUMZUMZUNZUIWLWRGUMZUOZUJBUOZVTZUDWGWLGUMZUOZUEWIUOZUHBUOZUFBUOZVTZU + GBUOZHFKLULZIDUMZUMZEJKULZIDUMZUMZHFEYALDUMZUMZJLULZIDUMZUMZUNZACURUQZX + QPYJXQUGUFUHUJBCDUEUDUIGURMNOUSUTVAAXPYIUGJBQAWHJUNZVTZXOYIWJYLXNYIUFKB + AKBUQYKRVBYLWGKUNZVTZXMYIUHLBALBUQYKYMSVCYNWLLUNZVTZXLYIUEEWIYPEJKGUMZW + IAEYQUQYKYMYOTVKYPWHJWGKGAYKYMYOVDYLYMYOVEVFVGYPWFEUNZVTZXJYIUDFXKYSFKL + GUMZXKAFYTUQYKYMYOYRUAVHYSWGKWLLGYLYMYOYRVDYNYOYRVEVFVGYSWEFUNZVTZXIYIW + OUUBXHYIUJIBAIBUQYKYMYOYRUUAUBVIUUBWRIUNZVTZXFYIUIHXGUUDHLIGUMZXGAHUUEU + QYKYMYOYRUUAUUCUCVJUUDWLLWRIGYNYOYRUUAUUCVLUUBUUCVMVFVGUUDWPHUNZVTZXBYC + XEYHUUGWTXTWFEXAYBUUGWKYAWRIDUUGWHJWGKAYKYMYOYRUUAUUCUUFVNZYLYMYOYRUUAU + UCUUFVOZVPZUUBUUCUUFVEZVFUUGWPHWEFWSXSUUGWQXRWRIDUUGWGKWLLUUIYNYOYRUUAU + UCUUFVQZVPUUKVFUUDUUFVMZYSUUAUUCUUFVDZVRYPYRUUAUUCUUFVLZVRUUGWPHWNYEXDY + GUUGXCYFWRIDUUGWHJWLLUUHUULVPUUKVFUUMUUGWEFWFEWMYDUUGWKYAWLLDUUJUULVFUU + NUUOVRVRWAVSWBWCWBWBWBWBWCWBWD $. + $} + + catcone0.f $e |- ( ph -> ( X H Y ) =/= (/) ) $. + catcone0.g $e |- ( ph -> ( Y H Z ) =/= (/) ) $. + $( Composition of non-empty hom-sets is non-empty. (Contributed by Zhi + Wang, 18-Sep-2024.) $) + catcone0 $p |- ( ph -> ( X H Z ) =/= (/) ) $= + ( vg vf wex cv cop co wcel c0 wa n0 anbi12i exdistrv sylbb2 syl2anc ancli + wne 19.42vv biimpri ccat adantr simprl simprr catcocl 2eximi exlimivv syl + 3syl ne0i ) ARUAZSUAZFGUBHDUCUCZFHEUCZUDZRTSTZVIUEUMZAAVGFGEUCZUDZVFGHEUC + ZUDZUFZRTSTZUFZAVQUFZRTSTZVKAVRAVMUEUMZVOUEUMZVRPQWBWCUFVNSTZVPRTZUFVRWBW + DWCWESVMUGRVOUGUHVNVPSRUIUJUKULWAVSAVQSRUNUOVTVJSRVTBCDVGVFEFGHIJKACUPUDV + QLUQAFBUDVQMUQAGBUDVQNUQAHBUDVQOUQAVNVPURAVNVPUSUTVAVDVJVLSRVIVHVEVBVC $. $} ${ @@ -443917,6 +443968,15 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the latexdef "Sphere" as "\mathrm{Sphere}"; /* End of Alexander van der Vekens's mathbox */ +/* Mathbox of Zhi Wang */ +htmldef "ThinCat" as "ThinCat"; + althtmldef "ThinCat" as "ThinCat"; + latexdef "ThinCat" as "\mathrm{ThinCat}"; +htmldef "ProsetToCat" as "ProsetToCat"; + althtmldef "ProsetToCat" as "ProsetToCat"; + latexdef "ProsetToCat" as "\mathrm{ProsetToCat}"; +/* End of Zhi Wang's mathbox */ + /* Mathbox of Emmett Weisz */ htmldef "setrecs" as "setrecs"; althtmldef "setrecs" as "setrecs"; @@ -464529,17 +464589,6 @@ and the expression ( x e. A /\ x e. B ) ` . -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - ${ - $d x y A $. - $( "At most one" element in a set. (Contributed by Thierry Arnoux, - 26-Jul-2018.) $) - moel $p |- ( E* x x e. A <-> A. x e. A A. y e. A x = y ) $= - ( cv wcel weq wi wal wmo ralcom4 df-ral ralbii wa alcom eleq1w mo4 impexp - wral albii bitr4i 3bitr4i 3bitr4ri ) BDCEZABFZGZBHZACRUEACRZBHZUDBCRZACRA - DCEZAIZUEABCJUIUFACUDBCKLUJUCMUDGZBHAHULAHZBHUKUHULABNUJUCABABCOPUGUMBUGU - JUEGZAHUMUEACKULUNAUJUCUDQSTSUAUB $. - $} - ${ $d i j x $. mo5f.1 $e |- F/ i ph $. @@ -646006,14 +646055,6 @@ D Fn ( I ... ( M - 1 ) ) /\ ( wi wo jao syl6c ) ABCDHEDHCEIDHFGCDEJK $. $} - ${ - sylibda.1 $e |- ( ph -> ( ps <-> ch ) ) $. - sylibda.2 $e |- ( ( ph /\ ch ) -> th ) $. - $( A syllogism deduction. (Contributed by SN, 16-Jul-2024.) $) - sylibda $p |- ( ( ph /\ ps ) -> th ) $= - ( biimpa syldan ) ABCDABCEGFH $. - $} - ${ syl3an12.1 $e |- ( ph -> ps ) $. syl3an12.2 $e |- ( ch -> th ) $. @@ -647662,7 +647703,7 @@ proof usage (see ~ mplelbas and ~ mpladd ). Note that hypothesis 0 is uneq2d adantr mpteq1d eqtr3d syl5eq anbi12d grpcl syl3an1 simprll simprrl cof 3expb off ffnd wfn fnconstg mp1i difexd cin c0 disjdif ofun fvconst2g inidm sylan grplid syl2anc sylancom wb eleq1d eqtr4d offveq eqtrd caovclg - adantrrl adantrll eqeltrrd sylibda fsuppind elmapd mpbird ifeq1d mpteq2dv + adantrrl adantrll eqeltrrd sylbida fsuppind elmapd mpbird ifeq1d mpteq2dv mpdan fveq1 elrab3 fsuppssindlem1 bitr4d mpbid ) AKFUNZUHIUHUOZFUPZUVAUIU OZUQZLURZUSZHUPZUIDFUTVAZVBZUPZKHUPZAFDUUTVEZUUTLVCVFZWJUVJAUVLUVMAIDFKUE UAVDZAKVGFLUFLVGUPZALGVHQVIZVJZVKVLAMUJDEGUVIFVGUUTLNOPQRSAFIJTUAVMZAFLVN @@ -775662,6 +775703,30 @@ additional condition (deduction form). See ~ ralbidc for a more ( wa wrex anim1i r19.41v sylibr ) ACGBDEHZCGBCGDEHALCFIBCDEJK $. $} + $( 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. ) $= + ( cv wcel wex wtru wa wrex tru biantru exbii df-rex bitr4i ) ACBDZAENFGZAEF + ABHNOAFNIJKFABLM $. + + $( Two ways of expressing "at most one" element. (Contributed by Zhi Wang, + 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.) $) + rmotru $p |- ( E* x x e. A <-> E* x e. A T. ) $= + ( cv wcel wmo wtru wa wrmo tru biantru mobii df-rmo bitr4i ) ACBDZAENFGZAEF + ABHNOAFNIJKFABLM $. + + $( Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, + 23-Sep-2024.) $) + reutru $p |- ( E! x x e. A <-> E! x e. A T. ) $= + ( cv wcel weu wtru wa wreu tru biantru eubii df-reu bitr4i ) ACBDZAENFGZAEF + ABHNOAFNIJKFABLM $. + + $( Alternate proof for ~ reutru . (Contributed by Zhi Wang, 23-Sep-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + reutruALT $p |- ( E! x x e. A <-> E! x e. A T. ) $= + ( cv wcel wex wmo wa wtru wrex wrmo weu rextru rmotru anbi12i df-eu 3bitr4i + wreu reu5 ) ACBDZAEZSAFZGHABIZHABJZGSAKHABQTUBUAUCABLABMNSAOHABRP $. + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -775719,6 +775784,147 @@ additional condition (deduction form). See ~ ralbidc for a more $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Unordered and ordered pairs +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $( The singleton of the universal class is the empty set. (Contributed by + Zhi Wang, 19-Sep-2024.) $) + vsn $p |- { _V } = (/) $= + ( cvv wcel wn csn c0 wceq vprc snprc mpbi ) AABCADEFGAHI $. + + ${ + $d A x z $. $d A y z $. $d B x $. + $( "At most one" element in a singleton. (Contributed by Zhi Wang, + 19-Sep-2024.) $) + mosn $p |- ( A = { B } -> E* x x e. A ) $= + ( csn wceq cv wcel wmo wtru wrmo rmosn rmotru mpbir eleq2 mobidv mpbiri ) + BCDZEZAFZBGZAHSQGZAHZUBIAQJIACKAQLMRTUAABQSNOP $. + + $( "At most one" element in an empty set. (Contributed by Zhi Wang, + 19-Sep-2024.) $) + mo0 $p |- ( A = (/) -> E* x x e. A ) $= + ( c0 wceq cvv csn cv wcel wmo vsn eqcomi eqeq1 mpbiri mosn syl ) BCDZBEFZ + DZAGBHAIPRCQDQCJKBCQLMABENO $. + + $( "At most one" element in a subclass of a singleton. (Contributed by Zhi + Wang, 23-Sep-2024.) $) + mosssn $p |- ( A C_ { B } -> E* x x e. A ) $= + ( csn wss c0 wceq wo cv wcel wmo sssn mo0 mosn jaoi sylbi ) BCDZEBFGZBQGZ + HAIBJAKZBCLRTSABMABCNOP $. + + $( Two ways of expressing "at most one" element in a class. (Contributed + by Zhi Wang, 19-Sep-2024.) $) + mo0sn $p |- ( E* x x e. A <-> ( A = (/) \/ E. y A = { y } ) ) $= + ( vz cv wcel wmo c0 wceq csn wex wo nfv eleq1w cbvmow wn wa wb wal weu + neq0 anbi1i df-eu eu6 dfcleq velsn bibi2i albii sylbbr eximi sylbi expcom + 3bitr2i orrd mo0 mosn exlimiv jaoi impbii bitri ) AECFZAGDEZCFZDGZCHIZCBE + ZJZIZBKZLZVAVCADVADMVCAMADCNOVDVJVDVEVIVEPZVDVIVKVDQZVCVBVFIZRZDSZBKZVIVL + VCDKZVDQVCDTVPVKVQVDDCUAUBVCDUCVCDBUDUMVOVHBVHVCVBVGFZRZDSVODCVGUEVSVNDVR + VMVCDVFUFUGUHUIUJUKULUNVEVDVIDCUOVHVDBDCVFUPUQURUSUT $. + + $( Two ways of expressing "at most one" element in a class. (Contributed + by Zhi Wang, 23-Sep-2024.) $) + mosssn2 $p |- ( E* x x e. A <-> E. y A C_ { y } ) $= + ( c0 wceq cv csn wo wex wss wcel wmo 19.45v sssn exbii mo0sn 3bitr4ri ) C + DEZCBFZGZEZHZBIRUABIHCTJZBIAFCKALRUABMUCUBBCSNOABCPQ $. + $} + + ${ + $d A g $. $d f g $. $d B f $. + $( There is at most one function into the empty set. (Contributed by Zhi + Wang, 19-Sep-2024.) $) + mof0 $p |- E* f f : A --> (/) $= + ( vg c0 cv wf wmo wceq wi wal wex 0ex eqeq2 imbi2d albidv f00 simplbi mpg + spcev df-mo mpbir ) ADBEZFZBGUCUBCEZHZIZBJZCKZUCUBDHZIZUHBUGUJBJCDLUDDHZU + FUJBUKUEUIUCUDDUBMNOSUCUIADHAUBPQRUCBCTUA $. + + $( A variant of ~ mof0 . (Contributed by Zhi Wang, 20-Sep-2024.) $) + mof02 $p |- ( B = (/) -> E* f f : A --> B ) $= + ( c0 wceq cv wf wmo mof0 feq3 mobidv mpbiri ) BDEZABCFZGZCHADNGZCHACIMOPC + BDANJKL $. + $} + + ${ + $d A f g $. + $( Alternate proof for ~ mof0 with stronger requirements on distinct + variables. Uses ~ mo4 . (Contributed by Zhi Wang, 19-Sep-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + mof0ALT $p |- E* f f : A --> (/) $= + ( vg c0 cv wf wmo wa wceq wi wal f00 simplbi eqtr3 syl2an gen2 feq1 mpbir + mo4 ) ADBEZFZBGUAADCEZFZHTUBIZJZCKBKUEBCUATDIZUBDIZUDUCUAUFADIZATLMUCUGUH + AUBLMTUBDNOPUAUCBCADTUBQSR $. + $} + + ${ + $d A f g x $. $d B f g x $. $d f ph $. + eufsn.1 $e |- ( ph -> B e. W ) $. + ${ + eufsnlem.2 $e |- ( ph -> ( A X. { B } ) e. V ) $. + $( There is exactly one function into a singleton. For a simpler + hypothesis, see ~ eufsn assuming ~ ax-rep , or ~ eufsn2 assuming + ~ ax-pow and ~ ax-un . (Contributed by Zhi Wang, 19-Sep-2024.) $) + eufsnlem $p |- ( ph -> E! f f : A --> { B } ) $= + ( vg csn cv wf wceq wb wal wex weu cxp wcel syl fconst2g alrimiv bibi2d + eqeq2 albidv spcedv eu6im ) ABCJZDKZLZUIIKZMZNZDOZIPUJDQAUNUJUIBUHRZMZN + ZDOIEUOHAUQDACFSUQGBCFUIUATUBUKUOMZUMUQDURULUPUJUKUOUIUDUCUEUFUJDIUGT + $. + $} + + eufsn.2 $e |- ( ph -> A e. V ) $. + $( There is exactly one function into a singleton, assuming ~ ax-rep . See + ~ eufsn2 for different axiom requirements. If existence is not needed, + use ~ mofsn or ~ mofsn2 for fewer axiom assumptions. (Contributed by + Zhi Wang, 19-Sep-2024.) $) + eufsn $p |- ( ph -> E! f f : A --> { B } ) $= + ( vx cvv wcel csn cxp cmpt fconstmpt mptexg eqeltrid syl eufsnlem ) ABCDJ + FGABEKZBCLMZJKHTUAIBCNJIBCOIBCEPQRS $. + + $( There is exactly one function into a singleton, assuming ~ ax-pow and + ~ ax-un . Variant of ~ eufsn . If existence is not needed, use ~ mofsn + or ~ mofsn2 for fewer axiom assumptions. (Contributed by Zhi Wang, + 19-Sep-2024.) $) + eufsn2 $p |- ( ph -> E! f f : A --> { B } ) $= + ( cvv wcel csn cxp snex xpexg sylancl eufsnlem ) ABCDIFGABEJCKZIJBQLIJHCM + BQEINOP $. + $} + + ${ + $d A f g y $. $d B f g x y $. $d V f g $. $d Y f $. + $( There is at most one function into a singleton, with fewer axioms than + ~ eufsn and ~ eufsn2 . See also ~ mofsn2 . (Contributed by Zhi Wang, + 19-Sep-2024.) $) + mofsn $p |- ( B e. V -> E* f f : A --> { B } ) $= + ( vg wcel csn cv wf wa wceq wal wmo cxp fconst2g biimpd eqtr3 a1i syl2and + wi alrimivv feq1 mo4 sylibr ) BDFZABGZCHZIZAUFEHZIZJUGUIKZTZELCLUHCMUEULC + EUEUHUGAUFNZKZUJUIUMKZUKUEUHUNABDUGOPUEUJUOABDUIOPUNUOJUKTUEUGUIUMQRSUAUH + UJCEAUFUGUIUBUCUD $. + + $( There is at most one function into a singleton. An unconditional + variant of ~ mofsn , i.e., the singleton could be empty if ` Y ` is a + proper class. (Contributed by Zhi Wang, 19-Sep-2024.) $) + mofsn2 $p |- ( B = { Y } -> E* f f : A --> B ) $= + ( csn wceq cvv wcel cv wf wa mofsn adantl wb feq3 mobidv adantr mpbird c0 + wmo wn simpl snprc biimpi eqtrd mof02 syl pm2.61dan ) BDEZFZDGHZABCIZJZCT + ZUJUKKUNAUIULJZCTZUKUPUJADCGLMUJUNUPNUKUJUMUOCBUIAULOPQRUJUKUAZKZBSFUNURB + UISUJUQUBUQUISFZUJUQUSDUCUDMUEABCUFUGUH $. + + $( There is at most one function into a subclass of a singleton. + (Contributed by Zhi Wang, 24-Sep-2024.) $) + mofsssn $p |- ( B C_ { Y } -> E* f f : A --> B ) $= + ( csn wss c0 wceq wo cv wf wmo sssn mof02 mofsn2 jaoi sylbi ) BDEZFBGHZBR + HZIABCJKCLZBDMSUATABCNABCDOPQ $. + + $( There is at most one function into a class containing at most one + element. (Contributed by Zhi Wang, 19-Sep-2024.) $) + mofmo $p |- ( E* x x e. B -> E* f f : A --> B ) $= + ( vy cv wcel wmo c0 wceq csn wex wo mo0sn mof02 mofsn2 exlimiv jaoi sylbi + wf ) AFCGAHCIJZCEFZKJZELZMBCDFTDHZAECNUAUEUDBCDOUCUEEBCDUBPQRS $. + $} + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= ZF Set Theory - add the Axiom of Power Sets @@ -775740,6 +775946,120 @@ additional condition (deduction form). See ~ ralbidc for a more FOFCFIOBFDFBCFJBKLMN $. +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Operations +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + fvconstr.1 $e |- ( ph -> F = ( R X. { Y } ) ) $. + ${ + fvconstr.2 $e |- ( ph -> Y e. V ) $. + fvconstr.3 $e |- ( ph -> Y =/= (/) ) $. + $( Two ways of expressing ` A R B ` . (Contributed by Zhi Wang, + 18-Sep-2024.) $) + fvconstr $p |- ( ph -> ( A R B <-> ( A F B ) = Y ) ) $= + ( wbr cop wcel co wceq df-br wa adantr c0 wne csn oveqd df-ov fvconst2g + cxp cfv eqtrdi sylan eqtrd simpr eqnetrd wb neeq1d mpbid ndmfv necon1ai + cdm dmxpss sseldi syl impbida syl5bb ) BCDKBCLZDMZABCENZGOZBCDPAVDVFAVD + QVEVCDGUAZUEZUFZGAVEVIOVDAVEBCVHNVIAEVHBCHUBBCVHUCUGZRAGFMVDVIGOIDGVCFU + DUHUIAVFQZVISTZVDVKVESTZVLVKVEGSAVFUJAGSTVFJRUKAVMVLULVFAVEVISVJUMRUNVL + VHUQZDVCDVGURVCVNMVISVCVHUOUPUSUTVAVB $. + + $( Two ways of expressing ` A R B ` . (Contributed by Zhi Wang, + 20-Sep-2024.) $) + fvconstrn0 $p |- ( ph -> ( A R B <-> ( A F B ) =/= (/) ) ) $= + ( wbr cop wcel co c0 wne df-br wa wceq adantr csn oveqd df-ov fvconst2g + cxp cfv eqtrdi sylan eqtrd eqnetrd neeq1d biimpa dmxpss necon1ai sseldi + cdm ndmfv syl impbida syl5bb ) BCDKBCLZDMZABCENZOPZBCDQAVBVDAVBRZVCGOVE + VCVADGUAZUEZUFZGAVCVHSVBAVCBCVGNVHAEVGBCHUBBCVGUCUGZTAGFMVBVHGSIDGVAFUD + UHUIAGOPVBJTUJAVDRVHOPZVBAVDVJAVCVHOVIUKULVJVGUPZDVADVFUMVAVKMVHOVAVGUQ + UNUOURUSUT $. + $} + + ${ + fvconstr2.2 $e |- ( ph -> X e. ( A F B ) ) $. + $( Two ways of expressing ` A R B ` . (Contributed by Zhi Wang, + 18-Sep-2024.) $) + fvconstr2 $p |- ( ph -> A R B ) $= + ( cop wcel wbr co c0 wne ne0d csn cxp cfv oveqd df-ov eqtrdi neeq1d cdm + dmxpss ndmfv necon1ai sseldi syl6bi mpd df-br sylibr ) ABCJZDKZBCDLABCE + MZNOZUNAUOFIPAUPUMDGQZRZSZNOZUNAUOUSNAUOBCURMUSAEURBCHTBCURUAUBUCUTURUD + ZDUMDUQUEUMVAKUSNUMURUFUGUHUIUJBCDUKUL $. + $} + $} + + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + ZF Set Theory - add the Axiom of Union +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Equinumerosity +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + $d A x $. $d B x $. $d X x $. + fvconst0ci.1 $e |- B e. _V $. + fvconst0ci.2 $e |- Y = ( ( A X. { B } ) ` X ) $. + $( A constant function's value is either the constant or the empty set. + (An artifact of our function value definition.) (Contributed by Zhi + Wang, 18-Sep-2024.) $) + fvconst0ci $p |- ( Y = (/) \/ Y = B ) $= + ( csn cxp cdm wcel c0 wceq wo cfv dmxpss sseli fvconst2 syl syl5eq olcd + wn ndmfv orcd pm2.61i ) CABGZHZIZJZDKLZDBLZMUHUJUIUHDCUFNZBFUHCAJUKBLUGAC + AUEOPABCEQRSTUHUAZUIUJULDUKKFCUFUBSUCUD $. + $} + + ${ + $d A x $. $d B x $. $d X x $. + fvconstdomi.1 $e |- B e. _V $. + $( A constant function's value is dominated by the constant. (An artifact + of our function value definition.) (Contributed by Zhi Wang, + 18-Sep-2024.) $) + fvconstdomi $p |- ( ( A X. { B } ) ` X ) ~<_ B $= + ( csn cxp cdm wcel cfv cdom wbr wceq sseli fvconst2 syl cvv domrefg ax-mp + dmxpss eqbrtrdi wn c0 ndmfv 0dom pm2.61i ) CABEZFZGZHZCUGIZBJKUIUJBBJUICA + HUJBLUHACAUFSMABCDNOBPHBBJKDBPQRTUIUAUJUBBJCUGUCBDUDTUE $. + $} + + ${ + $d A y $. $d F y $. $d X y $. $d ph y $. $d x y $. + f1omo.1 $e |- ( ph -> F = ( A X. { 1o } ) ) $. + $( There is at most one element in the function value of a constant + function whose output is ` 1o ` . (An artifact of our function value + definition.) Proof could be significantly shortened by ~ fvconstdomi + assuming ~ ax-un (see ~ f1omoALT ). (Contributed by Zhi Wang, + 19-Sep-2024.) $) + f1omo $p |- ( ph -> E* y y e. ( F ` X ) ) $= + ( vx cv cfv wcel wmo c1o csn cxp c0 wceq wal el1o mobidv mpbiri 1oex eqid + wo fvconst0ci mo0 wa wi eqtr3 syl2anb gen2 eleq1w mo4 mpbir eleq2w2 ax-mp + jaoi fveq1d eleq2d ) ABHZEDIZJZBKUSECLMNZIZJZBKZVCOPZVCLPZUCVECLEVCUAVCUB + UDVFVEVGBVCUEVGVEUSLJZBKZVIVHGHZLJZUFUSVJPZUGZGQBQVMBGVHUSOPVJOPVLVKUSRVJ + RUSVJOUHUIUJVHVKBGBGLUKULUMVGVDVHBBVCLUNSTUPUOAVAVDBAUTVCUSAEDVBFUQURST + $. + $} + + ${ + $d F y $. $d X y $. + f1omoALT.1 $e |- ( ph -> F = ( A X. { 1o } ) ) $. + $( There is at most one element in the function value of a constant + function whose output is ` 1o ` . (An artifact of our function value + definition.) Use ~ f1omo without assuming ~ ax-un . (Contributed by + Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + f1omoALT $p |- ( ph -> E* y y e. ( F ` X ) ) $= + ( cfv c1o cdom wbr cv wcel wmo csn cxp fveq1d fvconstdomi eqbrtrdi modom2 + 1oex sylibr ) AEDGZHIJBKUBLBMAUBECHNOZGHIAEDUCFPCHETQRBUBSUA $. + $} + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Order sets @@ -776703,6 +777023,692 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Preordered sets and directed sets using extensible structures +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + $d K x y z $. $d ph x y z $. + isprsd.b $e |- ( ph -> B = ( Base ` K ) ) $. + isprsd.l $e |- ( ph -> .<_ = ( le ` K ) ) $. + isprsd.k $e |- ( ph -> K e. V ) $. + $( Property of being a preordered set (deduction form). (Contributed by + Zhi Wang, 18-Sep-2024.) $) + isprsd $p |- ( ph -> ( K e. Proset <-> A. x e. B A. y e. B A. z e. B + ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) $= + ( wcel cv cfv wbr wa wi wral breqd raleqbidv cproset cple cbs cvv wb eqid + elexd isprs baib syl anbi12d imbi12d bitr4d ) AFUALZBMZUOFUBNZOZUOCMZUPOZ + URDMZUPOZPZUOUTUPOZQZPZDFUCNZRZCVFRZBVFRZUOUOGOZUOURGOZURUTGOZPZUOUTGOZQZ + PZDERZCERZBERAFUDLZUNVIUEAFHKUGUNVSVIBCDVFFUPVFUFUPUFUHUIUJAVRVHBEVFIAVQV + GCEVFIAVPVEDEVFIAVJUQVOVDAGUPUOUOJSAVMVBVNVCAVKUSVLVAAGUPUOURJSAGUPURUTJS + UKAGUPUOUTJSULUKTTTUM $. + $} + + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + 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 $. + catprs.1 $e |- ( ph -> A. x e. B A. y e. B + ( x .<_ y <-> ( x H y ) =/= (/) ) ) $. + ${ + catprslem.x $e |- ( ph -> X e. B ) $. + catprslem.y $e |- ( ph -> Y e. B ) $. + $( Lemma for ~ catprs . (Contributed by Zhi Wang, 18-Sep-2024.) $) + catprslem $p |- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) $= + ( vz vw cv wbr co c0 wne wb wral breq1 oveq1 neeq1d bibi12d breq2 oveq2 + weq cbvral2vw sylib wcel wi wceq wa breq12 oveq12 rspc2gv syl2anc mpd ) + ALNZMNZFOZUSUTEPZQRZSZMDTLDTZGHFOZGHEPZQRZSZABNZCNZFOZVJVKEPZQRZSZCDTBD + TVEIVOVDUSVKFOZUSVKEPZQRZSBCLMDDBLUGZVLVPVNVRVJUSVKFUAVSVMVQQVJUSVKEUBU + CUDCMUGZVPVAVRVCVKUTUSFUEVTVQVBQVKUTUSEUFUCUDUHUIAGDUJHDUJVEVIUKJKVDVIL + MGHDDUSGULUTHULUMZVAVFVCVHUSGUTHFUNWAVBVGQUSGUTHEUOUCUDUPUQUR $. + $} + + catprs.b $e |- ( ph -> B = ( Base ` C ) ) $. + catprs.h $e |- ( ph -> H = ( Hom ` C ) ) $. + ${ + catprs.c $e |- ( ph -> C e. Cat ) $. + $( A preorder can be extracted from a category. See ~ catprs2 for more + details. (Contributed by Zhi Wang, 18-Sep-2024.) $) + catprs $p |- ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X + /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) ) $= + ( wcel wa wbr co c0 wne w3a wi ccid cfv chom eqid adantr simpr1 eleqtrd + cbs ccat wceq catidcl oveqd eleqtrrd ne0d cv wb wral catprslem ad2antrr + mpbird eleq2d pm5.32i cco simplr1 simplr2 simplr3 simpr2 biimpa adantrr + 3anbi123d eqnetrrd sylanbr simpr3 adantrl catcone0 sylanb eqnetrd jca + ex ) AHDOZIDOZJDOZUAZPZHHGQZHIGQZIJGQZPZHJGQZUBWFWGHHFRZSTWFWLHEUCUDZUD + ZWFWNHHEUEUDZRWLWFEUJUDZEWMWOHWPUFZWOUFZWMUFAEUKOZWENUGWFHDWPAWBWCWDUHZ + ADWPULWELUGUIUMWFFWOHHAFWOULZWEMUGUNUOUPWFBCDFGHHABUQZCUQZGQXBXCFRSTURC + DUSBDUSWEKUGZWTWTUTVBWFWJWKWFWJPZWKHJFRZSTZXEXFHJWORZSXEFWOHJAXAWEWJMVA + ZUNWFAHWPOZIWPOZJWPOZUAZPZWJXHSTAWEXMAWBXJWCXKWDXLADWPHLVCADWPILVCADWPJ + LVCVLVDZXNWJPWPEEVEUDZWOHIJWQWRXPUFAWSXMWJNVAXJXKXLAWJVFXJXKXLAWJVGXJXK + XLAWJVHXNWFWJHIWORZSTXOXEHIFRZXQSXEFWOHIXIUNWFWHXRSTZWIWFWHXSWFBCDFGHIX + DWTAWBWCWDVIZUTVJVKVMVNXNWFWJIJWORZSTXOXEIJFRZYASXEFWOIJXIUNWFWIYBSTZWH + WFWIYCWFBCDFGIJXDXTAWBWCWDVOZUTVJVPVMVNVQVRVSWFWKXGURWJWFBCDFGHJXDWTYDU + TUGVBWAVT $. + + ${ + $d B u v $. $d C u v w $. $d ph u v w $. + catprs2.l $e |- ( ph -> .<_ = ( le ` C ) ) $. + $( A category equipped with the induced preorder, where an object ` x ` + is defined to be "less than or equal to" ` y ` iff there is a + morphism from ` x ` to ` y ` , is a preordered set, or a proset. + The category might not be thin. See ~ catprsc and ~ catprsc2 for + constructions satisfying the hypothesis "catprs.1". See ~ catprs + for a more primitive version. See ~ prsthinc for constructing a + thin category from a proset. (Contributed by Zhi Wang, + 18-Sep-2024.) $) + catprs2 $p |- ( ph -> C e. Proset ) $= + ( vw vv vu cproset cv wbr wa wral wcel catprs ralrimivvva ccat isprsd + wi mpbird ) AEPUAMQZUHGRUHNQZGRUIOQZGRSUHUJGRUFSZODTNDTMDTAUKMNODDDAB + CDEFGUHUIUJHIJKUBUCAMNODEGUDILKUEUG $. + $} + +$( + catprs3.k @e |- ( ph -> K = ( C sSet <. ( le ` ndx ) , .<_ >. ) ) @. + @( A category equipped with the induced preorder is a preordered set, or + a proset. (Contributed by Zhi Wang, XX-Sep-2024.) @) + catprs3 @p |- ( ph -> K e. Proset ) @= + ( ) ? @. +$) + $} + +$( + catprs4.f @e |- ( ph -> F = ( c e. Cat |-> .<_ ) ) @. + @( There is a function from ` Cat ` to the class of preorders. + (Contributed by Zhi Wang, XX-Sep-2024.) @) + catprs4 @p |- ( ph -> F : Cat --> ( le " Proset ) ) @= + ( ) ? @. +$) + $} + + ${ + $d B w x y $. $d H x y $. $d ph w z $. $d x y z $. + catprsc.1 $e |- ( ph -> .<_ = { <. x , y >. | + ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) } ) $. + $( A construction of the preorder induced by a category. See ~ catprs2 for + details. See also ~ catprsc2 for an alternate construction. + (Contributed by Zhi Wang, 18-Sep-2024.) $) + catprsc $p |- ( ph -> A. z e. B A. w e. B + ( z .<_ w <-> ( z H w ) =/= (/) ) ) $= + ( cv wbr co c0 wne wcel wa w3a vex weq eleq1d wb copab breqd simpl oveq12 + simpr neeq1d 3anbi123d df-3an bitrdi eqid braba baibd ralrimivva ) ADJZEJ + ZHKZUOUPGLZMNZUADEFFAUQUOFOZUPFOZPZUSAUQUOUPBJZFOZCJZFOZVCVEGLZMNZQZBCUBZ + KVBUSPZAHVJUOUPIUCVIVKBCUOUPVJDRERBDSZCESZPZVIUTVAUSQVKVNVDUTVFVAVHUSVNVC + UOFVLVMUDTVNVEUPFVLVMUFTVNVGURMVCUOVEUPGUEUGUHUTVAUSUIUJVJUKULUJUMUN $. + $} + + ${ + $d B w $. $d H x y $. $d ph w z $. $d w x y z $. + catprsc2.1 $e |- ( ph -> .<_ = { <. x , y >. | ( x H y ) =/= (/) } ) $. + $( An alternate construction of the preorder induced by a category. See + ~ catprs2 for details. See also ~ catprsc for a different construction. + The two constructions are different because ~ df-cat does not require + the domain of ` H ` to be ` B X. B ` . (Contributed by Zhi Wang, + 23-Sep-2024.) $) + catprsc2 $p |- ( ph -> A. z e. B A. w e. B + ( z .<_ w <-> ( z H w ) =/= (/) ) ) $= + ( cv wbr co c0 wne wb wcel wa copab vex weq oveq12 neeq1d eqid ralrimivva + breqd braba bitrdi adantr ) ADJZEJZHKZUIUJGLZMNZOZDEFFAUNUIFPUJFPQAUKUIUJ + BJZCJZGLZMNZBCRZKUMAHUSUIUJIUEURUMBCUIUJUSDSESBDTCETQUQULMUOUIUPUJGUAUBUS + UCUFUGUHUD $. + $} + + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Examples of categories +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Thin categories +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $c ThinCat $. + + $( Extend class notation with the class of thin categories. $) + cthinc $a class ThinCat $. + + ${ + $d B b c f g h x y $. $d C b c f g h x y $. $d H b c f g h x y $. + $( Definition of the class of thin categories, or posetal categories, whose + hom-sets each contain at most one morphism. Example 3.26(2) of [Adamek] + p. 33. "ThinCat" was taken instead of "PosCat" because the latter might + mean the category of posets. (Contributed by Zhi Wang, 17-Sep-2024.) $) + df-thinc $a |- ThinCat = { c e. Cat | + [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. + A. x e. b A. y e. b E* f f e. ( x h y ) } $. + + isthinc.b $e |- B = ( Base ` C ) $. + isthinc.h $e |- H = ( Hom ` C ) $. + $( The predicate "is a thin category". (Contributed by Zhi Wang, + 17-Sep-2024.) $) + isthinc $p |- ( C e. ThinCat <-> + ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) $= + ( vh vb vc cv co wcel wmo wral chom cfv cbs wceq wsbc ccat cthinc eqtr4di + cvv fvexd fveq2 wa adantr wb raleq raleqbi1dv ad2antlr oveq eleq2d mobidv + 2ralbidv adantl bitrd sbcied2 df-thinc elrab2 ) ELZALZBLZILZMZNZEOZBJLZPZ + AVJPZIKLZQRZUAZJVMSRZUAVCVDVEFMZNZEOZBCPACPZKDUBUCVMDTZVOVTJVPCUEWAVMSUFW + AVPDSRCVMDSUGGUDWAVJCTZUHZVLVTIVNFUEWCVMQUFWAVNFTWBWAVNDQRFVMDQUGHUDUIWCV + FFTZUHVLVIBCPZACPZVTWBVLWFUJWAWDVKWEAVJCVIBVJCUKULUMWDWFVTUJWCWDVIVSABCCW + DVHVREWDVGVQVCVDVEVFFUNUOUPUQURUSUTUTABEIJKVAVB $. + + $( A thin category is a category in which all hom-sets have cardinality + less than or equal to the cardinality of ` 1o ` . (Contributed by Zhi + Wang, 17-Sep-2024.) $) + isthinc2 $p |- ( C e. ThinCat <-> + ( C e. Cat /\ A. x e. B A. y e. B ( x H y ) ~<_ 1o ) ) $= + ( vf cthinc wcel ccat cv co wmo wral wa c1o cdom wbr isthinc modom2 bitri + 2ralbii anbi2i ) DIJDKJZHLALBLEMZJHNZBCOACOZPUEUFQRSZBCOACOZPABCDHEFGTUHU + JUEUGUIABCCHUFUAUCUDUB $. + + $( A thin category is a category in which, given a pair of objects ` x ` + and ` y ` and any two morphisms ` f , g ` from ` x ` to ` y ` , the + morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024.) $) + isthinc3 $p |- ( C e. ThinCat <-> ( C e. Cat /\ + A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) ) $= + ( cthinc wcel ccat cv co wmo wral wa weq isthinc moel 2ralbii anbi2i + bitri ) DJKDLKZEMAMBMGNZKEOZBCPACPZQUDEFRFUEPEUEPZBCPACPZQABCDEGHISUGUIUD + UFUHABCCEFUETUAUBUC $. + $} + + ${ + $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 $. + $d Y k l $. $d Y k w $. $d k ph $. $d ph z $. + isthincd2lem1.1 $e |- ( ph -> X e. B ) $. + isthincd2lem1.2 $e |- ( ph -> Y e. B ) $. + isthincd2lem1.3 $e |- ( ph -> F e. ( X H Y ) ) $. + isthincd2lem1.4 $e |- ( ph -> G e. ( X H Y ) ) $. + ${ + isthincd2lem1.5 $e |- ( ph -> + A. x e. B A. y e. B E* f f e. ( x H y ) ) $. + $( Lemma for ~ isthincd2 and ~ thincmo2 . (Contributed by Zhi Wang, + 17-Sep-2024.) $) + isthincd2lem1 $p |- ( ph -> F = G ) $= + ( vk cv wceq wral wcel vl vz vw wmo oveq1 eleq2d mobidv oveq2 cbvral2vw + co sylib nfv eleq1w cbvmow syl5bb wa eqidd rspc2vd mpd moel eqeq1 eqeq2 + ) APQZUAQZRZUAIJHUJZSPVFSZFGRZAVCVFTZPUDZVGAEQZUBQZUCQZHUJZTZEUDZUCDSUB + DSZVJAVKBQZCQZHUJZTZEUDZCDSBDSVQOWBVPVKVLVSHUJZTZEUDBCUBUCDDVRVLRZWAWDE + WEVTWCVKVRVLVSHUEUFUGVSVMRZWDVOEWFWCVNVKVSVMVLHUHUFUGUIUKAVJVKIVMHUJZTZ + EUDZVPUBUCIJDDDVLIRZVOWHEWJVNWGVKVLIVMHUEUFUGWIVCWGTZPUDVMJRZVJWHWKEPWH + PULWKEULEPWGUMUNWLWKVIPWLWGVFVCVMJIHUHUFUGUOKAWJUPDUQLURUSPUAVFUTUKAVHF + VDRVEPUAFGVFVFVFVCFVDVAVDGFVBMAVCFRUPVFUQNURUS $. + $} + + ${ + $d B f $. $d C f x y $. + thincmo2.b $e |- B = ( Base ` C ) $. + thincmo2.h $e |- H = ( Hom ` C ) $. + thincmo2.c $e |- ( ph -> C e. ThinCat ) $. + $( Morphisms in the same hom-set are identical. (Contributed by Zhi + Wang, 17-Sep-2024.) $) + thincmo2 $p |- ( ph -> F = G ) $= + ( vx vy vf wcel cv cthinc co wmo wral isthinc simprbi syl isthincd2lem1 + ccat ) APQBRDEFGHIJKLACUASZRTPTQTFUBSRUCQBUDPBUDZOUJCUISUKPQBCRFMNUEUFU + GUH $. + $} + $} + + ${ + $d B f g x y $. $d C f g x y $. $d H f g x y $. $d X f g x y $. + $d Y f g x y $. $d f g ph $. + thincmo.c $e |- ( ph -> C e. ThinCat ) $. + thincmo.x $e |- ( ph -> X e. B ) $. + thincmo.y $e |- ( ph -> Y e. B ) $. + ${ + thincmo.b $e |- B = ( Base ` C ) $. + thincmo.h $e |- H = ( Hom ` C ) $. + $( There is at most one morphism in each hom-set. (Contributed by Zhi + Wang, 21-Sep-2024.) $) + thincmo $p |- ( ph -> E* f f e. ( X H Y ) ) $= + ( vg cv co wcel wa weq wal adantr wi simprl simprr thincmo2 ex alrimivv + wmo cthinc eleq1w mo4 sylibr ) ADNZFGEOZPZMNZUMPZQZDMRZUAZMSDSUNDUGAUSD + MAUQURAUQQBCULUOEFGAFBPUQITAGBPUQJTAUNUPUBAUNUPUCKLACUHPUQHTUDUEUFUNUPD + MDMUMUIUJUK $. + + $( Alternate proof for ~ thincmo . (Contributed by Zhi Wang, + 21-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + thincmoALT $p |- ( ph -> E* f f e. ( X H Y ) ) $= + ( vx vy cv co wcel wmo wral wceq cthinc ccat isthinc simprbi syl oveq12 + wi wa eleq2d mobidv rspc2gv syl2anc mpd ) ADOZMOZNOZEPZQZDRZNBSMBSZUNFG + EPZQZDRZACUAQZUTHVDCUBQUTMNBCDEKLUCUDUEAFBQGBQUTVCUGIJUSVCMNFGBBUOFTUPG + TUHZURVBDVEUQVAUNUOFUPGEUFUIUJUKULUM $. + $} + + thincn0eu.b $e |- ( ph -> B = ( Base ` C ) ) $. + thincn0eu.h $e |- ( ph -> H = ( Hom ` C ) ) $. + $( At most one morphism in each hom-set (deduction form). (Contributed by + Zhi Wang, 21-Sep-2024.) $) + thincmod $p |- ( ph -> E* f f e. ( X H Y ) ) $= + ( cv co wcel wmo chom cfv eleqtrd eqid thincmo oveqd eleq2d mobidv mpbird + cbs ) ADMZFGENZOZDPUGFGCQRZNZOZDPACUFRZCDUJFGHAFBUMIKSAGBUMJKSUMTUJTUAAUI + ULDAUHUKUGAEUJFGLUBUCUDUE $. + + $( In a thin category, a hom-set being non-empty is equivalent to having a + unique element. (Contributed by Zhi Wang, 21-Sep-2024.) $) + thincn0eu $p |- ( ph -> + ( ( X H Y ) =/= (/) <-> E! f f e. ( X H Y ) ) ) $= + ( co c0 wne cv wcel weu wa sylibr wex wmo n0 biimpi thincmod df-eu expcom + anim12i euex impbid1 ) AFGEMZNOZDPUKQZDRZULAUNULASUMDUAZUMDUBZSUNULUOAUPU + LUODUKUCZUDABCDEFGHIJKLUEUHUMDUFTUGUNUOULUMDUIUQTUJ $. + $} + + ${ + $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 $. + $d H f g k u v w z $. $d H g k l u v w z $. $d H f g w x y z $. + $d X k l u v w $. $d Y k l u v $. $d Z k l u $. $d v w y z $. + isthincd2lem2.1 $e |- ( ph -> X e. B ) $. + isthincd2lem2.2 $e |- ( ph -> Y e. B ) $. + isthincd2lem2.3 $e |- ( ph -> Z e. B ) $. + isthincd2lem2.4 $e |- ( ph -> F e. ( X H Y ) ) $. + isthincd2lem2.5 $e |- ( ph -> G e. ( Y H Z ) ) $. + isthincd2lem2.6 $e |- ( ph -> A. x e. B A. y e. B A. z e. B + A. f e. ( x H y ) A. g e. ( y H z ) + ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) $. + $( Lemma for ~ isthincd2 . (Contributed by Zhi Wang, 17-Sep-2024.) $) + isthincd2lem2 $p |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) $= + ( vl vk vw vv vu cv cop wcel wral wceq oveq1 opeq1 oveq1d eleq12d ralbidv + co oveqd raleqbidv oveq2 opeq2 eleq1d cbvral2vw bitrdi cbvral3vw sylib wi + rspc3v syl3anc mpd rspc2v syl2anc ) AUAUFZUBUFZLMUGZNFUPZUPZLNKUPZUHZUAMN + KUPZUIZUBLMKUPZUIZJIVOUPZVQUHZAVLVMUCUFZUDUFZUGZUEUFZFUPZUPZWEWHKUPZUHZUA + WFWHKUPZUIZUBWEWFKUPZUIZUEEUIUDEUIUCEUIZWBAHUFZGUFZBUFZCUFZUGZDUFZFUPZUPZ + WTXCKUPZUHZHXAXCKUPZUIZGWTXAKUPZUIZDEUICEUIBEUIWQTXKWPWRWSWEXAUGZXCFUPZUP + ZWEXCKUPZUHZHXHUIZGWEXAKUPZUIWRWSWGXCFUPZUPZXOUHZHWFXCKUPZUIZGWOUIZBCDUCU + DUEEEEWTWEUJZXIXQGXJXRWTWEXAKUKYEXGXPHXHYEXEXNXFXOYEXDXMWRWSYEXBXLXCFWTWE + XAULUMUQWTWEXCKUKUNUOURXAWFUJZXQYCGXRWOXAWFWEKUSYFXPYAHXHYBXAWFXCKUKYFXNX + TXOYFXMXSWRWSYFXLWGXCFXAWFWEUTUMUQVAURURXCWHUJZYDWRWSWIUPZWKUHZHWMUIZGWOU + IWPYGYCYJGWOYGYAYIHYBWMXCWHWFKUSYGXTYHXOWKYGXSWIWRWSXCWHWGFUSUQXCWHWEKUSU + NURUOYIWLWRVMWIUPZWKUHGHUBUAWOWMWSVMUJYHYKWKWSVMWRWIUSVAWRVLUJYKWJWKWRVLV + MWIUKVAVBVCVDVEALEUHMEUHNEUHWQWBVFOPQWPWBVLVMLWFUGZWHFUPZUPZLWHKUPZUHZUAW + MUIZUBLWFKUPZUIVLVMVNWHFUPZUPZYOUHZUAMWHKUPZUIZUBWAUIUCUDUELMNEEEWELUJZWN + YQUBWOYRWELWFKUKUUDWLYPUAWMUUDWJYNWKYOUUDWIYMVLVMUUDWGYLWHFWELWFULUMUQWEL + WHKUKUNUOURWFMUJZYQUUCUBYRWAWFMLKUSUUEYPUUAUAWMUUBWFMWHKUKUUEYNYTYOUUEYMY + SVLVMUUEYLVNWHFWFMLUTUMUQVAURURWHNUJZUUCVTUBWAUUFUUAVRUAUUBVSWHNMKUSUUFYT + VPYOVQUUFYSVOVLVMWHNVNFUSUQWHNLKUSUNURUOVGVHVIAIWAUHJVSUHWBWDVFRSVRWDVLIV + OUPZVQUHUBUAIJWAVSVMIUJVPUUGVQVMIVLVOUSVAVLJUJUUGWCVQVLJIVOUKVAVJVKVI $. + $} + + ${ + $d B y $. $d C f x y $. $d f ph x y $. + isthincd.b $e |- ( ph -> B = ( Base ` C ) ) $. + isthincd.h $e |- ( ph -> H = ( Hom ` C ) ) $. + isthincd.t $e |- ( ( ph /\ ( x e. B /\ y e. B ) ) + -> E* f f e. ( x H y ) ) $. + ${ + isthincd.c $e |- ( ph -> C e. Cat ) $. + $( The predicate "is a thin category" (deduction form). (Contributed by + Zhi Wang, 17-Sep-2024.) $) + isthincd $p |- ( ph -> C e. ThinCat ) $= + ( ccat wcel cv cfv co wmo wral raleqbidv eqid chom cbs ralrimivva oveqd + cthinc eleq2d mobidv mpbid isthinc sylanbrc ) AELMFNZBNZCNZEUAOZPZMZFQZ + CEUBOZRZBURRZEUEMKAUKULUMGPZMZFQZCDRZBDRUTAVCBCDDJUCAVDUSBDURHAVCUQCDUR + HAVBUPFAVAUOUKAGUNULUMIUDUFUGSSUHBCUREFUNURTUNTUIUJ $. + $} + + $d .1. f g k w x z $. $d .x. f g k w x y z $. $d B f g k w x y z $. + $d C f g k w x y z $. $d H f g k w x y z $. $d f g k ph w x y z $. + isthincd2.o $e |- ( ph -> .x. = ( comp ` C ) ) $. + isthincd2.c $e |- ( ph -> C e. V ) $. + isthincd2.ps $e |- ( ps <-> ( ( x e. B /\ y e. B /\ z e. B ) /\ + ( f e. ( x H y ) /\ g e. ( y H z ) ) ) ) $. + isthincd2.1 $e |- ( ( ph /\ y e. B ) -> .1. e. ( y H y ) ) $. + isthincd2.2 $e |- ( ( ph /\ ps ) -> + ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) $. + $( The predicate " ` C ` is a thin category" without knowing ` C ` is a + category (deduction form). The identity arrow operator is also provided + as a byproduct. (Contributed by Zhi Wang, 17-Sep-2024.) $) + isthincd2 $p |- ( ph -> ( C e. ThinCat + /\ ( Id ` C ) = ( y e. B |-> .1. ) ) ) $= + ( vw vk cthinc wcel ccid cfv cmpt wceq ccat cv co w3a wa 3an4anass anbi1i + 3anbi1i 3anass an4 3bitri df-3an anbi2i 3bitr4i bitr4i cop simpr1l syldan + simpr1r simpr31 sylbir ralrimivva ralrimivvva isthincd2lem2 isthincd2lem1 + wral bianass adantr wmo sylan2b simpr2l simpr32 3ad2antr1 simpr2r simpr33 + sylan2br iscatd2 simpld isthincd simprd jca ) AGUDUEGUFUGDFIUHUIZACDFGJLN + OPAGUJUEZWKABUBUKZFUEZUCUKZEUKZWMLULUEZUMZCDEUBFGHIJKUCLMNOQRWRCUKZFUEZDU + KZFUEZUNZWPFUEZWNUNZUNZJUKZWSXALULZUEZKUKZXAWPLULZUEZWQUMZUNZXCXEXMUMZWTX + BXDUMZWNUNZXIXLUNZWQUNZUNZXFXSUNWRXNXQXFXSWTXBXDWNUOUPWRXPXRUNZWNWQUMYAWN + WQUNUNXTBYAWNWQSUQYAWNWQURXPXRWNWQUSUTXMXSXFXIXLWQVAVBVCXCXEXMVAVDZTWRAXO + IXGWSXAVEZXAHULULZXGUIYBAXOUNZCDFJYDXGLWSXAWTXBXEXMAVFZWTXBXEXMAVHZYECDEF + HJKXGILWSXAXAYFYGYGXIXLWQXCXEAVIZAXOXBIXAXALULUEYGTVGZAXJXGYCWPHULULZWSWP + LULUEZKXKVOJXHVOZEFVODFVOCFVOXOAYLCDEFFFAXPUNZYKJKXHXKYMXRUNABUNYKBXPXRAS + VPUAVJVKVLVQZVMYHAXIJVRZDFVOCFVOXOAYOCDFFPVKVQZVNVSWRAXOXJIXAXAVEWPHULULZ + XJUIYBYECDFJYQXJLXAWPYGXDWNXCXMAVTZYECDEFHJKIXJLXAXAWPYGYGYRYIXIXLWQXCXEA + WAZYNVMYSYPVNVSAWNBYKWQUAWBZWRAXOWOXJXAWPVEWMHULULZXGYCWMHULULZWOYJWSWPVE + WMHULULZUIYBYECDFJUUBUUCLWSWMYFXDWNXCXMAWCZYECDEFHJKXGUUALWSXAWMYFYGUUDYH + YECDEFHJKXJWOLXAWPWMYGYRUUDYSXIXLWQXCXEAWDZYNVMYNVMYECDEFHJKYJWOLWSWPWMYF + YRUUDXOAWRYKYBYTWEUUEYNVMYPVNVSWFZWGWHAWLWKUUFWIWJ $. + $} + + ${ + $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 $. + $} + + $( 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 $. + $( Any structure with an empty set of objects is a thin category. + (Contributed by Zhi Wang, 17-Sep-2024.) $) + 0thincg $p |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. ThinCat ) $= + ( vf vx vy wcel c0 cbs cfv wceq wa ccat cv chom co wral cthinc 0catg eqid + wmo ral0 raleq mpbii adantl isthinc sylanbrc ) ABFZGAHIZJZKALFCMDMEMANIZO + FCTEUHPZDUHPZAQFABRUIULUGUIUKDGPULUKDUAUKDGUHUBUCUDDEUHACUJUHSUJSUEUF $. + $} + + $( The empty category (see ~ 0cat ) is thin. (Contributed by Zhi Wang, + 17-Sep-2024.) $) + 0thinc $p |- (/) e. ThinCat $= + ( c0 cvv wcel cbs cfv wceq cthinc 0ex base0 0thincg mp2an ) ABCAADEFAGCHIAB + JK $. + + ${ + $d .<_ f g x y z $. $d B f g x y z $. $d C f g x y z $. + $d f g ph x y z $. + indthinc.b $e |- ( ph -> B = ( Base ` C ) ) $. + ${ + indthinc.h $e |- ( ph -> ( ( B X. B ) X. { 1o } ) = ( Hom ` C ) ) $. + indthinc.o $e |- ( ph -> (/) = ( comp ` C ) ) $. + indthinc.c $e |- ( ph -> C e. V ) $. + $( An indiscrete category in which all hom-sets have exactly one morphism + is a thin category. Constructed here is an indiscrete category where + all morphisms are ` (/) ` . This is a special case of ~ prsthinc , + where ` .<_ = ( B X. B ) ` . This theorem also implies a functor from + the category of sets to the category of small categories. + (Contributed by Zhi Wang, 17-Sep-2024.) (Proof shortened by Zhi Wang, + 19-Sep-2024.) $) + indthinc $p |- ( ph + -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) ) $= + ( vx vz vf vg cv wcel c1o co wa c0 wceq w3a cxp csn cop cfv eqidd f1omo + wmo df-ov eleq2i mobii sylibr biid id ancli ovconst2 0lt1o eleq2 mpbiri + 1oex 3syl adantl a1i 0ov oveqi eqtri 3adant2 3eltr4d ad2antrl isthincd2 + ) AJNZCOZBNZCOZKNZCOZUAZLNZVKVMCCUBZPUCUBZQZOZMNZVMVOVTQORZRZJBKCDSSLMV + TEFGAVLVNRRZVRVKVMUDZVTUEZOZLUHWBLUHWFLVSVTWGWFVTUFUGWBWILWAWHVRVKVMVTU + IUJUKULHIWEUMVNSVMVMVTQZOZAVNVNVNRWJPTZWKVNVNVNUNUOCCPVMVMUTUPWLWKSPOZU + QWJPSURUSVAVBVQWCVRWGVOSQZQZVKVOVTQZOAWDVQSPWOWPWMVQUQVCWOSTVQWOWCVRSQS + WNSWCVRWGVOVDVEWCVRVDVFVCVLVPWPPTVNCCPVKVOUTUPVGVHVIVJ $. + + $( An alternate proof for ~ indthinc assuming more axioms including + ~ ax-pow and ~ ax-un . (Contributed by Zhi Wang, 17-Sep-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + indthincALT $p |- ( ph + -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) ) $= + ( vf cv wcel c1o co wa c0 cdom 1oex ovconst2 wceq vx vz w3a cxp csn wmo + vg wbr cvv domrefg ax-mp eqbrtrdi modom2 sylibr adantl biid ancli 0lt1o + id eleq2 mpbiri 3syl cop a1i 0ov oveqi eqtri 3adant2 ad2antrl isthincd2 + 3eltr4d ) AUAKZCLZBKZCLZUBKZCLZUCZJKZVLVNCCUDMUEUDZNZLZUGKZVNVPVTNLOZOZ + UABUBCDPPJUGVTEFGVMVOOZWBJUFZAWFWAMQUHWGWFWAMMQCCMVLVNRSMUILMMQUHRMUIUJ + UKULJWAUMUNUOHIWEUPVOPVNVNVTNZLZAVOVOVOOWHMTZWIVOVOVOUSUQCCMVNVNRSWJWIP + MLZURWHMPUTVAVBUOVRWCVSVLVNVCZVPPNZNZVLVPVTNZLAWDVRPMWNWOWKVRURVDWNPTVR + WNWCVSPNPWMPWCVSWLVPVEVFWCVSVEVGVDVMVQWOMTVOCCMVLVPRSVHVKVIVJ $. + $} + + ${ + prsthinc.h $e |- ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) ) $. + prsthinc.o $e |- ( ph -> (/) = ( comp ` C ) ) $. + prsthinc.l $e |- ( ph -> .<_ = ( le ` C ) ) $. + prsthinc.p $e |- ( ph -> C e. Proset ) $. + $( Preordered sets as categories. Similar to example 3.3(4.d) of + [Adamek] p. 24, but the hom-sets are not pairwise disjoint. One can + define a functor from the category of prosets to the category of small + thin categories. See ~ catprs and ~ catprs2 for inducing a preorder + from a category. Example 3.26(2) of [Adamek] p. 33 indicates that it + induces a bijection from the equivalence class of isomorphic small + thin categories to the equivalence class of order-isomorphic + preordered sets. (Contributed by Zhi Wang, 18-Sep-2024.) $) + prsthinc $p |- ( ph + -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) ) $= + ( vf cv wcel c1o co wa c0 wbr breqd a1i w3a csn cxp cproset cop cfv wmo + vx vz vg eqidd f1omo df-ov eleq2i mobii sylibr biid 0lt1o wceq cple cbs + eleq2d eqid prsref sylan sylbida biimpar syldan cvv 1oex fvconstr mpbid + wne 1n0 eleqtrrid 0ov oveqi eqtri eqeltri simpl adantr 3anbi123d biimpa + adantrr simprrl fvconstr2 biimpd sylc simprrr prstr syl112anc isthincd2 + biimprd ) AUHLZCMZBLZCMZUILZCMZUAZKLZWNWPENUBUCZOZMZUJLZWPWRXBOMZPZPZUH + BUICDQQKUJXBUDFGAWOWQPPZXAWNWPUEZXBUFZMZKUGXDKUGXIKEXBXJXIXBUKULXDXLKXC + XKXAWNWPXBUMUNUOUPHJXHUQAWQPZQNWPWPXBOZURXMWPWPERZXNNUSAWQWPWPDUTUFZRZX + OAWQWPDVAUFZMZXQACXRWPFVBZADUDMZXSXQJXRDXPWPXRVCZXPVCZVDVEVFAXOXQAEXPWP + WPISVGVHXMWPWPEXBVINXMXBUKNVIMZXMVJTNQVMZXMVNTVKVLVOAXHPZXEXAXJWRQOZOZN + WNWRXBOZYHQNYHXEXAQOQYGQXEXAXJWRVPVQXEXAVPVRURVSYFWNWRERZYINUSYFAWNWRXP + RZYJAXHVTZYFYAWNXRMZXSWRXRMZUAZWNWPXPRZWPWRXPRZYKAYAXHJWAAWTYOXGAWTYOAW + OYMWQXSWSYNACXRWNFVBXTACXRWRFVBWBWCWDYFAWNWPERZYPYLYFWNWPEXBXANYFXBUKZA + WTXDXFWEWFAYRYPAEXPWNWPISWGWHYFAWPWRERZYQYLYFWPWREXBXENYSAWTXDXFWIWFAYT + YQAEXPWPWRISWGWHXRDXPWNWPWRYBYCWJWKAYJYKAEXPWNWRISWMWHYFWNWREXBVINYSYDY + FVJTYEYFVNTVKVLVOWL $. + $} + $} + + ${ + $d U f p x y z $. $d f ph y z $. + setcthin.c $e |- ( ph -> C = ( SetCat ` U ) ) $. + setcthin.u $e |- ( ph -> U e. V ) $. + setcthin.x $e |- ( ph -> A. x e. U E* p p e. x ) $. + $( A category of sets all of whose objects contain at most one element is + thin. (Contributed by Zhi Wang, 20-Sep-2024.) $) + setcthin $p |- ( ph -> C e. ThinCat ) $= + ( vy vz vf cfv eqid cv wcel wa wmo mobidv adantr csetc chom setcbas eqidd + cthinc co wf weq elequ2 wral simprr rspcdva mofmo simprl elsetchom mpbird + syl ccat setccat isthincd eqeltrd ) ACDUAMZUEGAJKDVBLVBUBMZAVBDEVBNZHUCAV + CUDAJOZDPZKOZDPZQZQZLOZVEVGVCUFPZLRVEVGVKUGZLRZVJFOZVGPZFRZVNVJVOBOPZFRZV + QBDVGBKUHVRVPFBKFUISAVSBDUJVIITAVFVHUKZULFVEVGLUMUQVJVLVMLVJVBDVKVCEVEVGV + DADEPZVIHTVCNAVFVHUNVTUOSUPAWAVBURPHVBDEVDUSUQUTVA $. + $} + + ${ + $d x y z $. + $( The category ` ( SetCat `` 2o ) ` is thin. A special case of + ~ setcthin . (Contributed by Zhi Wang, 20-Sep-2024.) $) + setc2othin $p |- ( SetCat ` 2o ) e. ThinCat $= + ( vx vz vy c2o csetc cfv cthinc wcel wtru cvv eqidd 2oex a1i wmo wral csn + cv c0 wceq wo cpr wex elpri 0ex sneq eqeq2d spcev orim2i mo0sn 3syl df2o2 + biimpri eleq2s rgen setcthin mptru ) DEFZGHIAUQDJBIUQKDJHILMBQAQZHBNZADOI + USADUSURRRPZUAZDURVAHURRSZURUTSZTVBURCQZPZSZCUBZTZUSURRUTUCVCVGVBVFVCCRUD + VDRSVEUTURVDRUEUFUGUHUSVHBCURUIULUJUKUMUNMUOUP $. + $} + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Preordered sets as thin categories +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $c ProsetToCat $. + + $( Class function defining preordered sets as categories. $) + cprstc $a class ProsetToCat $. + + ${ + $d C f x y z $. $d H f $. $d K k x y z $. $d X f $. $d Y f $. + $d ph f x y z $. + $( Definition of the function converting a preordered set to a category. + Justified by ~ prsthinc . + + This definition is somewhat arbitrary. Example 3.3(4.d) of [Adamek] + p. 24 demonstrates an alternate definition with pairwise disjoint + hom-sets. The behavior of the function is defined entirely, up to + isomorphism, by ~ prstcnid , ~ prstchom , and ~ prstcthin . Other + important properties include ~ prstcbas , ~ prstcleval , ~ prstcle , + ~ prstcocval , ~ prstcoc , ~ prstchom2 , and ~ prstcprs . Use those + instead. + + Note that the defining property ~ prstchom is equivalent to ~ prstchom2 + given ~ prstcthin . See ~ thincn0eu for justification. + + "ProsetToCat" was taken instead of "ProsetCat" because the latter might + mean the category of preordered sets (classes). However, "ProsetToCat" + seems too long. (Contributed by Zhi Wang, 20-Sep-2024.) + (New usage is discouraged.) $) + df-prstc $a |- ProsetToCat = ( k e. Proset |-> ( ( k sSet + <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet + <. ( comp ` ndx ) , (/) >. ) ) $. + + prstcnid.c $e |- ( ph -> C = ( ProsetToCat ` K ) ) $. + prstcnid.k $e |- ( ph -> K e. Proset ) $. + $( Lemma for ~ prstcnidlem and ~ prstcthin . (Contributed by Zhi Wang, + 20-Sep-2024.) (New usage is discouraged.) $) + prstcval $p |- ( ph -> C = ( ( K sSet + <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet + <. ( comp ` ndx ) , (/) >. ) ) $= + ( vk cprstc cfv cnx chom cple c1o csn cxp cop csts co cco cproset wceq c0 + wcel cv fveq2 xpeq1d opeq2d oveq12d oveq1d df-prstc ovex fvmpt syl eqtrd + id ) ABCGHZCIJHZCKHZLMZNZOZPQZIRHUAOZPQZDACSUBUOVCTEFCFUCZUPVDKHZURNZOZPQ + ZVBPQVCSGVDCTZVHVAVBPVIVDCVGUTPVIUNVIVFUSUPVIVEUQURVDCKUDUEUFUGUHFUIVAVBP + UJUKULUM $. + + ${ + prstcnid.e $e |- E = Slot ( E ` ndx ) $. + prstcnid.no $e |- ( E ` ndx ) =/= ( comp ` ndx ) $. + $( Lemma for ~ prstcnid and ~ prstchomval . (Contributed by Zhi Wang, + 20-Sep-2024.) (New usage is discouraged.) $) + prstcnidlem $p |- ( ph -> ( E ` C ) = ( E ` ( K sSet + <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) ) $= + ( cfv cnx chom cple c1o csn cxp cop csts co cco c0 prstcval setsnid + fveq2d eqtr4di ) ABCIDJKIDLIMNOPQRZJSIZTPQRZCIUECIABUGCABDEFUAUCTUFCUEG + HUBUD $. + + prstcnid.nh $e |- ( E ` ndx ) =/= ( Hom ` ndx ) $. + $( Components other than ` Hom ` and ` comp ` are unchanged. + (Contributed by Zhi Wang, 20-Sep-2024.) $) + prstcnid $p |- ( ph -> ( E ` K ) = ( E ` C ) ) $= + ( cfv cnx chom cple c1o csn cxp cop csts co setsnid prstcnidlem eqtr4id + ) ADCJDKLJZDMJNOPZQRSCJBCJUDUCCDGITABCDEFGHUAUB $. + $} + + ${ + prstcbas.b $e |- ( ph -> B = ( Base ` K ) ) $. + $( The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) $) + prstcbas $p |- ( ph -> B = ( Base ` C ) ) $= + ( cbs cfv baseid cnx chom wne slotsbhcdif simp2i simp1i prstcnid eqtrd + cco ) ABDHICHIGACHDEFJKHIZKLIZMZTKSIZMZUAUCMZNOUBUDUENPQR $. + $} + + ${ + prstcle.l $e |- ( ph -> .<_ = ( le ` K ) ) $. + $( Value of the less-than-or-equal-to relation is unchanged. + (Contributed by Zhi Wang, 20-Sep-2024.) $) + prstcleval $p |- ( ph -> .<_ = ( le ` C ) ) $= + ( cple cfv cnx wne c1 cc0 cdc c5 10re 1nn0 0nn0 5nn c4 pleid cco nngt0i + declt ltneii plendx ccondx neeq12i mpbir chom 4nn homndx prstcnid eqtrd + ) ADCHIBHIGABHCEFUAJHIZJUBIZKLMNZLONZKUQURPLMOQRSOSUCUDUEUOUQUPURUFUGUH + UIUOJUJIZKUQLTNZKUQUTPLMTQRUKTUKUCUDUEUOUQUSUTUFULUHUIUMUN $. + + $( Value of the less-than-or-equal-to relation is unchanged. + (Contributed by Zhi Wang, 20-Sep-2024.) $) + prstcle $p |- ( ph -> ( X .<_ Y <-> X ( le ` C ) Y ) ) $= + ( cple cfv prstcleval breqd ) ADBJKEFABCDGHILM $. + $} + + ${ + prstcoc.oc $e |- ( ph -> ._|_ = ( oc ` K ) ) $. + $( Orthocomplementation is unchanged. (Contributed by Zhi Wang, + 20-Sep-2024.) $) + prstcocval $p |- ( ph -> ._|_ = ( oc ` C ) ) $= + ( coc cfv cnx wne c1 cdc c5 1nn0 declt ltneii ocndx neeq12i mpbir deccl + ocid cco nn0rei 5nn 1lt5 ccondx chom c4 4nn 1lt4 homndx prstcnid eqtrd + ) ADCHIBHIGABHCEFUBJHIZJUCIZKLLMZLNMZKUQURUQLLOOUAUDZLLNOOUEUFPQUOUQUPU + RRUGSTUOJUHIZKUQLUIMZKUQVAUSLLUIOOUJUKPQUOUQUTVARULSTUMUN $. + + $( Orthocomplementation is unchanged. (Contributed by Zhi Wang, + 20-Sep-2024.) $) + prstcoc $p |- ( ph -> ( ._|_ ` X ) = ( ( oc ` C ) ` X ) ) $= + ( coc cfv prstcocval fveq1d ) AEDBIJABCDFGHKL $. + $} + + ${ + prstchomval.l $e |- ( ph -> .<_ = ( le ` C ) ) $. + $( Hom-sets of the constructed category which depend on an arbitrary + definition. (Contributed by Zhi Wang, 20-Sep-2024.) + (New usage is discouraged.) $) + prstchomval $p |- ( ph -> + ( .<_ X. { 1o } ) = ( Hom ` C ) ) $= + ( chom cfv cnx cple c1o csn cxp cop homid wne cproset wcel cvv csts cbs + co cco slotsbhcdif simp3i prstcnidlem wceq fvex snex xpex sylancl eqidd + setsid prstcleval eqtr4d xpeq1d 3eqtr2rd ) ABHICJHIZCKIZLMZNZOUAUCHIZVB + DVANABHCEFPJUBIZUSQVDJUDIZQUSVEQUEUFUGACRSVBTSVBVCUHFUTVACKUILUJUKRVBHT + CPUNULAUTDVAAUTBKIDABCUTEFAUTUMUOGUPUQUR $. + $} + + $( The category is a preordered set. (Contributed by Zhi Wang, + 20-Sep-2024.) $) + prstcprs $p |- ( ph -> C e. Proset ) $= + ( vx vy vz cproset wcel cv cple cfv wbr wa wral cvv eqidd cprstc isprsd + wi cbs prstcbas prstcleval fvex eqeltrdi bitr4d mpbird ) ABIJZCIJZEAUIFKZ + UKCLMZNUKGKZULNUMHKZULNOUKUNULNUAOHCUBMZPGUOPFUOPUJAFGHUOBULQAUOBCDEAUORZ + UCABCULDEAULRZUDABCSMQDCSUEUFTAFGHUOCULIUPUQETUGUH $. + + $( The preordered set is equipped with a thin category. (Contributed by + Zhi Wang, 20-Sep-2024.) $) + prstcthin $p |- ( ph -> C e. ThinCat ) $= + ( vy cthinc wcel ccid cfv c0 wceq cple eqidd cnx cop csts co cco cvv cmpt + cbs prstchomval chom c1o csn cxp ovex ccoid setsid mp2an prstcval eqtr4id + 0ex fveq2d prstcprs prsthinc simpld ) ABGHBIJFBUBJZKUALAFUSBBMJZAUSNABCUT + DEAUTNZUCAKCOUDJCMJUEUFUGPZQRZOSJKPQRZSJZBSJVCTHKTHKVELCVBQUHUNTKSTVCUIUJ + UKABVDSABCDEULUOUMVAABCDEUPUQUR $. + + ${ + prstchom.l $e |- ( ph -> .<_ = ( le ` C ) ) $. + prstchom.e $e |- ( ph -> H = ( Hom ` C ) ) $. + ${ + prstchom.x $e |- ( ph -> X e. ( Base ` C ) ) $. + prstchom.y $e |- ( ph -> Y e. ( Base ` C ) ) $. + $( Hom-sets of the constructed category are dependent on the preorder. + + Note that prstchom.x and prstchom.y are redundant here due to our + definition of ` ProsetToCat ` . However, this should not be assumed + as it is definition-dependent. Therefore, the two hypotheses are + added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024.) $) + prstchom $p |- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) ) $= + ( cvv c1o chom cfv csn cxp a1i prstchomval eqtr4d wcel wne fvconstrn0 + 1oex c0 1n0 ) AFGECNOACBPQEORSKABDEHIJUAUBONUCAUFTOUGUDAUHTUE $. + + $( Hom-sets of the constructed category are dependent on the preorder. + + Note that prstchom.x and prstchom.y are redundant here due to our + definition of ` ProsetToCat ` ( see ~ prstchom2ALT ). However, this + should not be assumed as it is definition-dependent. Therefore, the + two hypotheses are added for explicitness. (Contributed by Zhi + Wang, 21-Sep-2024.) $) + prstchom2 $p |- ( ph -> ( X .<_ Y <-> E! f f e. ( X H Y ) ) ) $= + ( wbr co c0 wne cv wcel weu prstchom prstcthin eqidd thincn0eu bitrd + cbs cfv ) AGHFOGHDPZQRCSUITCUAABDEFGHIJKLMNUBABUGUHZBCDGHABEIJUCMNAUJ + UDLUEUF $. + $} + + $( Hom-sets of the constructed category are dependent on the preorder. + This proof depends on the definition ~ df-prstc . See ~ prstchom2 for + a version that does not depend on the definition. (Contributed by Zhi + Wang, 20-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + prstchom2ALT $p |- ( ph -> ( X .<_ Y <-> E! f f e. ( X H Y ) ) ) $= + ( wbr cv wcel c1o cvv a1i c0 wne weu cen wceq ovex chom cfv prstchomval + co csn cxp eqtr4d 1oex 1n0 fvconstr biimpa eqeng mpsyl euen1b sylib wex + wa euex n0 sylibr fvconstrn0 biimpar sylan2 impbida ) AGHFMZCNGHDUHZOZC + UAZAVIVAZVJPUBMZVLVJQOVMVJPUCZVNGHDUDAVIVOAGHFDQPADBUEUFFPUIUJLABEFIJKU + GUKZPQOAULRZPSTAUMRZUNUOVJPQUPUQCVJURUSVLAVJSTZVIVLVKCUTVSVKCVBCVJVCVDA + VIVSAGHFDQPVPVQVRVEVFVGVH $. + $} + $} + $( (End of Zhi Wang's mathbox.) $) $( End $[ set-mbox-zw.mm $] $)