Skip to content

Commit

Permalink
Added thin category and preordered sets (metamath#4220)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@zwang123
zwang123 authored Sep 23, 2024
1 parent a8680d4 commit ff48fe1
Show file tree
Hide file tree
Showing 3 changed files with 1,108 additions and 72 deletions.
2 changes: 2 additions & 0 deletions changes-set.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
28 changes: 28 additions & 0 deletions discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand All @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down
Loading

0 comments on commit ff48fe1

Please sign in to comment.