Added thin category and preordered sets (metamath#4220)

* 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

@@ -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