Merge branch 'develop' of https://github.com/metamath/set.mm into dev…

…elop

.gitignore

@@ -1,4 +1,11 @@
 *~*
 mm.log
 *.demo.html
+,errs
+mmcomplex.html
+mmdeduction.html
 mmil.html
+mmnatded.html
+mmnf.html
+mmset.html
+mmzfcnd.html

discouraged

@@ -9357,7 +9357,6 @@
 "ltmpi" is used by "ltsonq".
 "ltneOLD" is used by "coprm".
 "ltneOLD" is used by "ltlen".
-"ltneOLD" is used by "ltnei".
 "ltneOLD" is used by "phibndlem".
 "ltneOLD" is used by "sineq0".
 "ltneOLD" is used by "stadd3i".
@@ -13792,6 +13791,7 @@ New usage of "5oalem5" is discouraged (1 uses).
 New usage of "5oalem6" is discouraged (1 uses).
 New usage of "5oalem7" is discouraged (1 uses).
 New usage of "a1iiOLD" is discouraged (0 uses).
+New usage of "a2andOLD" is discouraged (0 uses).
 New usage of "abbi1dvOLD" is discouraged (0 uses).
 New usage of "abbiOLD" is discouraged (0 uses).
 New usage of "abeq1iOLD" is discouraged (0 uses).
@@ -16752,7 +16752,7 @@ New usage of "ltexprlem6" is discouraged (1 uses).
 New usage of "ltexprlem7" is discouraged (1 uses).
 New usage of "ltmnq" is discouraged (11 uses).
 New usage of "ltmpi" is discouraged (5 uses).
-New usage of "ltneOLD" is discouraged (7 uses).
+New usage of "ltneOLD" is discouraged (6 uses).
 New usage of "ltpiord" is discouraged (7 uses).
 New usage of "ltprord" is discouraged (6 uses).
 New usage of "ltpsrpr" is discouraged (1 uses).
@@ -17031,6 +17031,7 @@ New usage of "nabbiOLD" is discouraged (0 uses).
 New usage of "naecoms-o" is discouraged (1 uses).
 New usage of "natded" is discouraged (0 uses).
 New usage of "nbgraopALT" is discouraged (0 uses).
+New usage of "nbiorOLD" is discouraged (0 uses).
 New usage of "necon1abidOLD" is discouraged (0 uses).
 New usage of "necon1abiiOLD" is discouraged (0 uses).
 New usage of "necon1adOLD" is discouraged (0 uses).
@@ -17413,6 +17414,7 @@ New usage of "ordelordALT" is discouraged (0 uses).
 New usage of "ordelordALTVD" is discouraged (0 uses).
 New usage of "ordpinq" is discouraged (6 uses).
 New usage of "ordpipq" is discouraged (5 uses).
+New usage of "ornldOLD" is discouraged (0 uses).
 New usage of "orthcom" is discouraged (6 uses).
 New usage of "orthin" is discouraged (2 uses).
 New usage of "osum" is discouraged (0 uses).
@@ -17760,6 +17762,8 @@ New usage of "rb-ax3" is discouraged (8 uses).
 New usage of "rb-ax4" is discouraged (6 uses).
 New usage of "rb-bijust" is discouraged (1 uses).
 New usage of "rb-imdf" is discouraged (4 uses).
+New usage of "rbaibOLD" is discouraged (0 uses).
+New usage of "rbaibrOLD" is discouraged (0 uses).
 New usage of "rblem1" is discouraged (4 uses).
 New usage of "rblem2" is discouraged (3 uses).
 New usage of "rblem3" is discouraged (1 uses).
@@ -18495,6 +18499,7 @@ Proof modification of "3ornot23" is discouraged (28 steps).
 Proof modification of "3ornot23VD" is discouraged (74 steps).
 Proof modification of "a1ii" is discouraged (9 steps).
 Proof modification of "a1iiOLD" is discouraged (8 steps).
+Proof modification of "a2andOLD" is discouraged (83 steps).
 Proof modification of "abbi1dvOLD" is discouraged (24 steps).
 Proof modification of "abbiOLD" is discouraged (88 steps).
 Proof modification of "abeq1iOLD" is discouraged (19 steps).
@@ -19410,6 +19415,7 @@ Proof modification of "mvridlemOLD" is discouraged (129 steps).
 Proof modification of "nabbiOLD" is discouraged (63 steps).
 Proof modification of "naecoms-o" is discouraged (19 steps).
 Proof modification of "nbgraopALT" is discouraged (271 steps).
+Proof modification of "nbiorOLD" is discouraged (23 steps).
 Proof modification of "necon1abidOLD" is discouraged (18 steps).
 Proof modification of "necon1abiiOLD" is discouraged (16 steps).
 Proof modification of "necon1adOLD" is discouraged (18 steps).
@@ -19508,6 +19514,7 @@ Proof modification of "orbi1r" is discouraged (9 steps).
 Proof modification of "orbi1rVD" is discouraged (101 steps).
 Proof modification of "ordelordALT" is discouraged (128 steps).
 Proof modification of "ordelordALTVD" is discouraged (202 steps).
+Proof modification of "ornldOLD" is discouraged (25 steps).
 Proof modification of "p0exALT" is discouraged (2 steps).
 Proof modification of "pm110.643" is discouraged (72 steps).
 Proof modification of "pm110.643ALT" is discouraged (35 steps).
@@ -19567,6 +19574,8 @@ Proof modification of "rb-ax3" is discouraged (12 steps).
 Proof modification of "rb-ax4" is discouraged (14 steps).
 Proof modification of "rb-bijust" is discouraged (55 steps).
 Proof modification of "rb-imdf" is discouraged (27 steps).
+Proof modification of "rbaibOLD" is discouraged (16 steps).
+Proof modification of "rbaibrOLD" is discouraged (16 steps).
 Proof modification of "rblem1" is discouraged (57 steps).
 Proof modification of "rblem2" is discouraged (31 steps).
 Proof modification of "rblem3" is discouraged (29 steps).

iset-discouraged

@@ -43,9 +43,12 @@
 "alrimih" is used by "sb4or".
 "alrimih" is used by "sb6rf".
 "alrimih" is used by "sbbid".
+"ax-0id" is used by "addid1".
 "ax-10o" is used by "ax10".
+"ax-1re" is used by "1re".
 "ax-addass" is used by "addass".
 "ax-addcl" is used by "addcl".
+"ax-addcom" is used by "addcom".
 "ax-addrcl" is used by "readdcl".
 "ax-cnex" is used by "cnex".
 "ax-cnre" is used by "cnre".
@@ -56,10 +59,15 @@
 "ax-mulcl" is used by "mulcl".
 "ax-mulcom" is used by "mulcom".
 "ax-mulrcl" is used by "remulcl".
+"axltirr" is used by "ltnr".
+"axlttrn" is used by "lttr".
 "axresscn" is used by "ax1cn".
 "df-ilim" is used by "dflim2".
 "df-iom" is used by "dfom3".
 "df-iord" is used by "dford3".
+"df-mnf" is used by "mnfnre".
+"df-pnf" is used by "mnfnre".
+"df-pnf" is used by "pnfnre".
 "df-tru" is used by "tru".
 "equsalh" is used by "dvelimALT".
 "equsalh" is used by "dvelimfALT2".
@@ -153,6 +161,8 @@
 "snexgOLD" is used by "uniop".
 "spimh" is used by "spim".
 "spimth" is used by "equveli".
+New usage of "0cnALT" is discouraged (0 uses).
+New usage of "0reALT" is discouraged (0 uses).
 New usage of "19.21h" is discouraged (3 uses).
 New usage of "19.21ht" is discouraged (2 uses).
 New usage of "19.41h" is discouraged (5 uses).
@@ -161,11 +171,14 @@ New usage of "19.9hd" is discouraged (2 uses).
 New usage of "4syl" is discouraged (6 uses).
 New usage of "a9evsep" is discouraged (1 uses).
 New usage of "alrimih" is discouraged (25 uses).
+New usage of "ax-0id" is discouraged (1 uses).
 New usage of "ax-10o" is discouraged (1 uses).
 New usage of "ax-11o" is discouraged (0 uses).
 New usage of "ax-16" is discouraged (0 uses).
+New usage of "ax-1re" is discouraged (1 uses).
 New usage of "ax-addass" is discouraged (1 uses).
 New usage of "ax-addcl" is discouraged (1 uses).
+New usage of "ax-addcom" is discouraged (1 uses).
 New usage of "ax-addrcl" is discouraged (1 uses).
 New usage of "ax-cnex" is discouraged (1 uses).
 New usage of "ax-cnre" is discouraged (1 uses).
@@ -175,19 +188,24 @@ New usage of "ax-mulass" is discouraged (1 uses).
 New usage of "ax-mulcl" is discouraged (1 uses).
 New usage of "ax-mulcom" is discouraged (1 uses).
 New usage of "ax-mulrcl" is discouraged (1 uses).
+New usage of "ax0id" is discouraged (0 uses).
 New usage of "ax0lt1" is discouraged (0 uses).
 New usage of "ax10" is discouraged (0 uses).
 New usage of "ax1cn" is discouraged (0 uses).
+New usage of "ax1re" is discouraged (0 uses).
 New usage of "ax1rid" is discouraged (0 uses).
 New usage of "ax9vsep" is discouraged (0 uses).
 New usage of "axaddass" is discouraged (0 uses).
 New usage of "axaddcl" is discouraged (0 uses).
+New usage of "axaddcom" is discouraged (0 uses).
 New usage of "axaddrcl" is discouraged (0 uses).
 New usage of "axcnex" is discouraged (0 uses).
 New usage of "axcnre" is discouraged (0 uses).
 New usage of "axdistr" is discouraged (0 uses).
 New usage of "axi2m1" is discouraged (0 uses).
 New usage of "axicn" is discouraged (0 uses).
+New usage of "axltirr" is discouraged (1 uses).
+New usage of "axlttrn" is discouraged (1 uses).
 New usage of "axmulass" is discouraged (0 uses).
 New usage of "axmulcl" is discouraged (0 uses).
 New usage of "axmulcom" is discouraged (0 uses).
@@ -211,6 +229,8 @@ New usage of "bocardo" is discouraged (0 uses).
 New usage of "df-ilim" is discouraged (1 uses).
 New usage of "df-iom" is discouraged (1 uses).
 New usage of "df-iord" is discouraged (1 uses).
+New usage of "df-mnf" is discouraged (1 uses).
+New usage of "df-pnf" is discouraged (2 uses).
 New usage of "df-tru" is discouraged (1 uses).
 New usage of "dftru2" is discouraged (0 uses).
 New usage of "difidALT" is discouraged (0 uses).
@@ -240,6 +260,8 @@ New usage of "spimth" is discouraged (1 uses).
 New usage of "strcollnfALT" is discouraged (0 uses).
 New usage of "truanOLD" is discouraged (0 uses).
 New usage of "xpexgALT" is discouraged (0 uses).
+Proof modification of "0cnALT" is discouraged (49 steps).
+Proof modification of "0reALT" is discouraged (15 steps).
 Proof modification of "a9evsep" is discouraged (63 steps).
 Proof modification of "ax9vsep" is discouraged (19 steps).
 Proof modification of "axi12" is discouraged (47 steps).