Finish removing +c from set.mm (#3558)

* Revise dmdprdpr and dprdpr in set.mm

Change from +c to a pair of ordered pairs in stating the theorems and in
the proofs.  Other than that the proofs are unchanged.

* Remove xpscfcda from set.mm

No longer used and replaced by xpscf

* Remove xpsfrnel2cda from set.mm

No longer used and replaced by xpsfrnel2

* Remove xpsc1 from set.mm

No longer used and replaced by fvpr1o

* Remove xpsc0 from set.mm

No longer used and replaced by fvpr0o

* Remove xpscfn from set.mm

No longer used and replaced by fnpr2o

* Revise df-xps in set.mm

Change the definition to use a pair of ordered pairs instead of +c .
This is the same as what had been a theorem dfxpspr so remove that
theorem and update its one usage to refer to df-xps .

* Remove xpscg from set.mm

No longer used.

* Remove xpsc from set.mm

No longer used.

* Remove cdadju from set.mm

As there is no +c left we can just recommend |_| .

* Remove cdaval from set.mm

Move most of its comment to a section header for the Cardinal number
arithmetic section (with some tweaks to the wording).

cdaval has no more usages so we can just refer people to df-dju instead.

* Remove df-cda and +c from set.mm

No longer used.  Remove the definition and the syntax and recommend
df-dju instead.

changes-set.txt

@@ -26,6 +26,20 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
  6-Oct-23 vtocl2d   [same]      moved from TA's mathbox to main set.mm
+ 4-Oct-23 df-cda    df-dju      use |_| instead of +c
+ 4-Oct-23 cdaval    df-dju      use |_| instead of +c
+ 4-Oct-23 cdadju    ---         use |_| instead of +c
+ 4-Oct-23 xpsc      ---         +c is no longer used or needed
+ 4-Oct-23 xpscg     ---         +c is no longer used or needed
+ 4-Oct-23 dfxpspr   df-xps      changes from +c to a pair of ordered pairs
+ 4-Oct-23 df-xps    [same]      changes from +c to a pair of ordered pairs
+ 4-Oct-23 xpscfn    fnpr2o      changes from +c to a pair of ordered pairs
+ 4-Oct-23 xpsc0     fvpr0o      changes from +c to a pair of ordered pairs
+ 4-Oct-23 xpsc1     fvpr1o      changes from +c to a pair of ordered pairs
+ 4-Oct-23 xpsfrnel2cda xpsfrnel2 changes from +c to a pair of ordered pairs
+ 4-Oct-23 xpscfcda  xpscf       changes from +c to a pair of ordered pairs
+ 4-Oct-23 dprdpr    [same]      changes from +c to a pair of ordered pairs
+ 4-Oct-23 dmdprdpr  [same]      changes from +c to a pair of ordered pairs
  2-Oct-23 xpsfeqcda xpsfeq      changes from +c to a pair of ordered pairs
  2-Oct-23 xpscfv    fvprif      changes from +c to a pair of ordered pairs
  2-Oct-23 xpsfvalcda xpsfval    changes from +c to a pair of ordered pairs

discouraged

@@ -2975,8 +2975,6 @@
 "ccshOLD" is used by "0csh0OLD".
 "ccshOLD" is used by "cshfnOLD".
 "ccshOLD" is used by "cshnzOLD".
-"cdaval" is used by "cdadju".
-"cdaval" is used by "xpsc".
 "cdj3lem1" is used by "cdj3i".
 "cdj3lem1" is used by "cdj3lem2b".
 "cdj3lem2" is used by "cdj3i".
@@ -4410,7 +4408,6 @@
 "df-c" is used by "opelcn".
 "df-c" is used by "wuncn".
 "df-cbn" is used by "iscbn".
-"df-cda" is used by "cdaval".
 "df-ch" is used by "isch".
 "df-ch0" is used by "df0op2".
 "df-ch0" is used by "elch0".
@@ -14253,7 +14250,6 @@ New usage of "ccats1swrdeqOLD" is discouraged (2 uses).
 New usage of "ccats1swrdeqbiOLD" is discouraged (0 uses).
 New usage of "ccats1swrdeqrexOLD" is discouraged (1 uses).
 New usage of "ccshOLD" is discouraged (3 uses).
-New usage of "cdaval" is discouraged (2 uses).
 New usage of "cdj1i" is discouraged (0 uses).
 New usage of "cdj3i" is discouraged (0 uses).
 New usage of "cdj3lem1" is discouraged (2 uses).
@@ -14746,7 +14742,6 @@ New usage of "df-bnj19" is discouraged (5 uses).
 New usage of "df-bra" is discouraged (3 uses).
 New usage of "df-c" is discouraged (12 uses).
 New usage of "df-cbn" is discouraged (1 uses).
-New usage of "df-cda" is discouraged (1 uses).
 New usage of "df-ch" is discouraged (1 uses).
 New usage of "df-ch0" is discouraged (8 uses).
 New usage of "df-chj" is discouraged (1 uses).