Remove same-alphabet requirement from ccatval1 (#3788)

* ccats1val1: remove antecedent of sethood of S
* ccat2s1p1: remove antecedent of sethood of Y
* ccat2s1p2: remove antecedent of sethood of X

Co-authored-by: avekens <[email protected]>

changes-set.txt

@@ -118,6 +118,9 @@ DONE:
 Date      Old       New         Notes
 23-Jan-24 nelb      [same]      moved from TA's mathbox to main set.mm
 22-Jan-24 syl6sseqr sseqtrrdi
+21-Jan-24 ccats1val1 [same]     revised - eliminated unnecessary antecedent
+21-Jan-24 ccat2s1p1 [same]      revised - eliminated unnecessary antecedent
+21-Jan-24 ccat2s1p2 [same]      revised - eliminated unnecessary antecedent
 20-Jan-24 nfiund    nfiundg
 20-Jan-24 bnj1441   bnj1441g
 20-Jan-24 cbviinv   cbviinvg
@@ -140,6 +143,8 @@ Date      Old       New         Notes
 17-Jan-24 mteqand   [same]      moved from SN's mathbox to main set.mm
 15-Jan-24 sseqtr4d  sseqtrrd
 14-Jan-24 sseqtr4i  sseqtrri
+14-Jan-24 ccat2s1len [same]     revised - eliminated unnecessary antecedents
+14-Jan-24 wlklenvclwlk [same]   revised - eliminated unnecessary antecedent
 13-Jan-24 mndlsmidm [same]      moved from AV's mathbox to main set.mm
 13-Jan-24 smndlsmidm [same]     moved from AV's mathbox to main set.mm
 13-Jan-24 cycsubm   [same]      moved from AV's mathbox to main set.mm

discouraged

@@ -18214,7 +18214,7 @@ Proof modification of "cbvexsv" is discouraged (29 steps).
 Proof modification of "cbvexvOLD" is discouraged (38 steps).
 Proof modification of "cbvrabvOLD" is discouraged (19 steps).
 Proof modification of "cbvrexdva2OLD" is discouraged (128 steps).
-Proof modification of "ccat2s1fvwALT" is discouraged (149 steps).
+Proof modification of "ccat2s1fvwALT" is discouraged (150 steps).
 Proof modification of "ceqsalgALT" is discouraged (58 steps).
 Proof modification of "ceqsexgvOLD" is discouraged (10 steps).
 Proof modification of "chordthmALT" is discouraged (440 steps).
@@ -18773,7 +18773,7 @@ Proof modification of "ghomlinOLD" is discouraged (161 steps).
 Proof modification of "grpinvfvalALT" is discouraged (161 steps).
 Proof modification of "grposnOLD" is discouraged (291 steps).
 Proof modification of "grpsubfvalALT" is discouraged (189 steps).
-Proof modification of "gsumccatOLD" is discouraged (995 steps).
+Proof modification of "gsumccatOLD" is discouraged (996 steps).
 Proof modification of "hadcomaOLD" is discouraged (37 steps).
 Proof modification of "hashge3el3dif" is discouraged (229 steps).
 Proof modification of "hba1-o" is discouraged (34 steps).