compositions of functions

* ~sylibda, ~ineqcom, ~ineqcomi, ~freld, ~fco3 (renamed) moved from mathboxes to main; proofs for ~funcofd (formerly ~fco3) and ~smfco shortened
* new theorem ~cnvimassrndm (generalization of ~cnvimarndm), proofs for ~cnvimarndm, ~fimacnv shortened
* new theorem ~ffrnb (generalization of ~ffrn)
* new theorems ~fncofn, ~fcof, ~f1cof1 (generalizations of ~fnco, ~fco, f1co), proofs shortened
* new theorems ~cnvimainrn , ~rescnvimafod added

AV's mathbox:
* comment for ~fsetabsnop  revised (as proposed by GL)
* new theorems ~fcores, ~fcoresf1,  ~fcoresfo1, ~fcoresfo2 and lemmas added
* new theorems ~f1cof1b, ~focofob, ~f1ocof1ob added

changes-set.txt

@@ -98,6 +98,11 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+20-Sep-24 fco3      funcofd     moved from GS's mathbox to main set.mm
+20-Sep-24 freld     [same]      moved from GS's mathbox to main set.mm
+20-Sep-24 ineqcomi  [same]      moved from PM's mathbox to main set.mm
+20-Sep-24 ineqcom   [same]      moved from PM's mathbox to main set.mm
+20-Sep-24 sylibda   [same]      moved from SN'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

discouraged

@@ -16089,12 +16089,15 @@ New usage of "exinst01" is discouraged (1 uses).
 New usage of "exinst11" is discouraged (1 uses).
 New usage of "exlimexi" is discouraged (2 uses).
 New usage of "expcomdg" is discouraged (0 uses).
+New usage of "f1coOLD" 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 "f1oweALT" is discouraged (0 uses).
 New usage of "f1rhm0to0ALT" is discouraged (0 uses).
 New usage of "falnorfalOLD" is discouraged (0 uses).
+New usage of "fco3OLD" is discouraged (0 uses).
+New usage of "fcoOLD" is discouraged (0 uses).
 New usage of "fdmOLD" is discouraged (0 uses).
 New usage of "festinoALT" is discouraged (0 uses).
 New usage of "fh1" is discouraged (3 uses).
@@ -16105,13 +16108,15 @@ New usage of "fh3i" is discouraged (1 uses).
 New usage of "fh4i" is discouraged (0 uses).
 New usage of "ficardun2OLD" is discouraged (0 uses).
 New usage of "ficardunOLD" is discouraged (0 uses).
+New usage of "fimacnvOLD" is discouraged (0 uses).
 New usage of "fimadmfoALT" is discouraged (0 uses).
 New usage of "findOLD" is discouraged (0 uses).
 New usage of "findcard2OLD" is discouraged (0 uses).
 New usage of "fldcALTV" is discouraged (0 uses).
 New usage of "fldcatALTV" is discouraged (1 uses).
 New usage of "flddivrng" is discouraged (2 uses).
 New usage of "fldhmsubcALTV" is discouraged (0 uses).
+New usage of "fncoOLD" is discouraged (0 uses).
 New usage of "fnexALT" is discouraged (0 uses).
 New usage of "fnresiOLD" is discouraged (0 uses).
 New usage of "fnsnfvOLD" is discouraged (0 uses).
@@ -19555,6 +19560,7 @@ Proof modification of "exinst" is discouraged (12 steps).
 Proof modification of "exinst01" is discouraged (16 steps).
 Proof modification of "exinst11" is discouraged (21 steps).
 Proof modification of "exlimexi" is discouraged (15 steps).
+Proof modification of "f1coOLD" is discouraged (99 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).
@@ -19563,13 +19569,17 @@ Proof modification of "f1rhm0to0ALT" is discouraged (161 steps).
 Proof modification of "falimfal" is discouraged (6 steps).
 Proof modification of "falimtru" is discouraged (6 steps).
 Proof modification of "falnorfalOLD" is discouraged (28 steps).
+Proof modification of "fco3OLD" is discouraged (60 steps).
+Proof modification of "fcoOLD" is discouraged (98 steps).
 Proof modification of "fdmOLD" is discouraged (19 steps).
 Proof modification of "festinoALT" is discouraged (24 steps).
 Proof modification of "ficardun2OLD" is discouraged (137 steps).
 Proof modification of "ficardunOLD" is discouraged (127 steps).
+Proof modification of "fimacnvOLD" is discouraged (78 steps).
 Proof modification of "fimadmfoALT" is discouraged (108 steps).
 Proof modification of "findOLD" is discouraged (70 steps).
 Proof modification of "findcard2OLD" is discouraged (535 steps).
+Proof modification of "fncoOLD" is discouraged (95 steps).
 Proof modification of "fnexALT" is discouraged (111 steps).
 Proof modification of "fnresiOLD" is discouraged (25 steps).
 Proof modification of "fnsnfvOLD" is discouraged (74 steps).