preimages, decompositions of function into a surjective and an inject…

…ive function (#3877)

* preimages, decompositions of function into a surjective and an injective function

Main:
* ~iuneqconst added
* ~uniexd  moved from GS' mathbox

AV's mathbox:
* auxiliary theorems for (pre)images
* theorems for the set of all preimages of function values
* decomposition of function into a surjective and an injective function with images as domain of the injective function

* formatting error (metamath-knife only!)

* replace cbvrexv/cbvralv by cbvrexvw/cbvralvw

* uniimafveqt, imaelsetpreimafv, fundcmpsurinj
* fiunlem

* fiunlemw/fiunw/f1iunw deleted

* proofs of fiunw/f1iunw copied to fiun/f1iun
* fiunlemw/fiunw/f1iunw deleted
* fiunw/f1iunw replaced by fiun/f1iun in proofs of ackbij2 and

All mentioned theorems do not depend on ax-13.

* Decomposition of functions into surjective, bijective and injective functions.

* funfvima2d (slightly revised and) moved from SP's mathbox to main set.mm (~imo72b2lem1 could have been shortened)
* ~uniimaelsetpreimafv revised (generalized)
* new theorem ~imasetpreimafvbij and corresponding new lemmas ~imasetpreimafvbijlemf, ~imasetpreimafvbijlemfo
* lemma ~fundcmpsurinjlem6 revised and renamed to ~imasetpreimafvbijlemf1
* new theorems ~fundcmpsurbijinjpreimafv and ~fundcmpsurbijinj
* proof of ~fundcmpsurinjpreimafv shortened using ~fundcmpsurbijinjpreimafv

* Typos

... detected by Gérard Lang.

* Typo

changes-set.txt

@@ -110,6 +110,8 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+23-Mar-24 funfvima2d [same]     moved from SP's mathbox to main set.mm
+17-Mar-24 uniexd    [same]      moved from GS's mathbox to main set.mm
 16-Mar-24 syl6eleq  eleqtrdi    compare to eleqtri or eleqtrd
 10-Mar-24 syl6eleqr eleqtrrdi   compare to eleqtrri or eleqtrrd
 29-Feb-24 syl6ss    sstrdi      compare to sstri or sstrd

discouraged

@@ -15270,6 +15270,7 @@ New usage of "funcringcsetclem7ALTV" is discouraged (1 uses).
 New usage of "funcringcsetclem8ALTV" is discouraged (1 uses).
 New usage of "funcringcsetclem9ALTV" is discouraged (1 uses).
 New usage of "funcrngcsetcALT" is discouraged (0 uses).
+New usage of "fundcmpsurinjALT" is discouraged (0 uses).
 New usage of "fvimacnvALT" is discouraged (0 uses).
 New usage of "gcdmultipleOLD" is discouraged (0 uses).
 New usage of "gcdmultiplezOLD" is discouraged (0 uses).
@@ -18768,6 +18769,7 @@ Proof modification of "frege98" is discouraged (116 steps).
 Proof modification of "frgrwopreglem5ALT" is discouraged (519 steps).
 Proof modification of "fsplitOLD" is discouraged (234 steps).
 Proof modification of "funcrngcsetcALT" is discouraged (765 steps).
+Proof modification of "fundcmpsurinjALT" is discouraged (221 steps).
 Proof modification of "fvilbdRP" is discouraged (27 steps).
 Proof modification of "fvimacnvALT" is discouraged (102 steps).
 Proof modification of "gcdmultipleOLD" is discouraged (348 steps).