shorten cgsex4g (#4593)

* shorten cgsex4g * shorten ceqsex * add versions of ceqsex/ceqsal avoiding df-clab * rewrap * add a revision tag * typos * add tags showing independence of df-clab
metamath · Jan 23, 2025 · 43acbdd · 43acbdd
1 parent e299d46
commit 43acbdd
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 95 deletions.
diff --git a/discouraged b/discouraged
@@ -3259,15 +3259,12 @@
 "cbvrexf" is used by "cbvrex".
 "cbvrexsv" is used by "cbvexsv".
 "cbvrexv" is used by "cbvrex2v".
-"cbvrexv" is used by "cygablOLD".
 "cbvrexv" is used by "rexlimdvaacbv".
 "cbvriota" is used by "cbvriotav".
 "cbvrmo" is used by "cbvrmov".
 "cbvsbc" is used by "cbvcsb".
 "cbvsbc" is used by "cbvsbcv".
 "ccat2s1fvwOLD" is used by "ccat2s1fstOLD".
-"ccatval1OLD" is used by "ccat2s1p1OLD".
-"ccatval1OLD" is used by "ccats1val1OLD".
 "ccatw2s1assOLD" is used by "ccat2s1fvwOLD".
 "ccatw2s1assOLD" is used by "ccatw2s1ccatws2OLD".
 "ccatw2s1ccatws2OLD" is used by "ccat2s1fvwALTOLD".
@@ -15384,7 +15381,7 @@ New usage of "cbvrexcsf" is discouraged (1 uses).
 New usage of "cbvrexdva2OLD" is discouraged (0 uses).
 New usage of "cbvrexf" is discouraged (1 uses).
 New usage of "cbvrexsv" is discouraged (1 uses).
-New usage of "cbvrexv" is discouraged (3 uses).
+New usage of "cbvrexv" is discouraged (2 uses).
 New usage of "cbvrexv2" is discouraged (0 uses).
 New usage of "cbvriota" is discouraged (1 uses).
 New usage of "cbvriotav" is discouraged (0 uses).
@@ -15398,10 +15395,6 @@ New usage of "ccat2s1fstOLD" is discouraged (0 uses).
 New usage of "ccat2s1fvwALT" is discouraged (0 uses).
 New usage of "ccat2s1fvwALTOLD" is discouraged (0 uses).
 New usage of "ccat2s1fvwOLD" is discouraged (1 uses).
-New usage of "ccat2s1p1OLD" is discouraged (0 uses).
-New usage of "ccat2s1p2OLD" is discouraged (0 uses).
-New usage of "ccats1val1OLD" is discouraged (0 uses).
-New usage of "ccatval1OLD" is discouraged (2 uses).
 New usage of "ccatw2s1assOLD" is discouraged (2 uses).
 New usage of "ccatw2s1ccatws2OLD" is discouraged (1 uses).
 New usage of "ccatw2s1p1OLD" is discouraged (0 uses).
@@ -15539,6 +15532,7 @@ New usage of "cdleml5N" is discouraged (0 uses).
 New usage of "cdlemm10N" is discouraged (0 uses).
 New usage of "ceqsalgALT" is discouraged (0 uses).
 New usage of "ceqsalvOLD" is discouraged (0 uses).
+New usage of "ceqsexOLD" is discouraged (0 uses).
 New usage of "ceqsexvOLD" is discouraged (0 uses).
 New usage of "ceqsexvOLDOLD" is discouraged (0 uses).
 New usage of "ceqsralvOLD" is discouraged (0 uses).
@@ -15850,7 +15844,6 @@ New usage of "cvr2N" is discouraged (1 uses).
 New usage of "cvrletrN" is discouraged (0 uses).
 New usage of "cvrnrefN" is discouraged (0 uses).
 New usage of "cvrval4N" is discouraged (0 uses).
-New usage of "cygablOLD" is discouraged (0 uses).
 New usage of "dalem31N" is discouraged (0 uses).
 New usage of "daraptiALT" is discouraged (0 uses).
 New usage of "dariiALT" is discouraged (0 uses).
@@ -20123,16 +20116,13 @@ Proof modification of "ccat2s1fstOLD" is discouraged (43 steps).
 Proof modification of "ccat2s1fvwALT" is discouraged (116 steps).
 Proof modification of "ccat2s1fvwALTOLD" is discouraged (150 steps).
 Proof modification of "ccat2s1fvwOLD" is discouraged (203 steps).
-Proof modification of "ccat2s1p1OLD" is discouraged (93 steps).
-Proof modification of "ccat2s1p2OLD" is discouraged (162 steps).
-Proof modification of "ccats1val1OLD" is discouraged (38 steps).
-Proof modification of "ccatval1OLD" is discouraged (145 steps).
 Proof modification of "ccatw2s1assOLD" is discouraged (48 steps).
 Proof modification of "ccatw2s1ccatws2OLD" is discouraged (57 steps).
 Proof modification of "ccatw2s1p1OLD" is discouraged (155 steps).
 Proof modification of "cchhllemOLD" is discouraged (157 steps).
 Proof modification of "ceqsalgALT" is discouraged (58 steps).
 Proof modification of "ceqsalvOLD" is discouraged (10 steps).
+Proof modification of "ceqsexOLD" is discouraged (49 steps).
 Proof modification of "ceqsexvOLD" is discouraged (47 steps).
 Proof modification of "ceqsexvOLDOLD" is discouraged (10 steps).
 Proof modification of "ceqsralvOLD" is discouraged (38 steps).
@@ -20193,7 +20183,6 @@ Proof modification of "currysetlem" is discouraged (49 steps).
 Proof modification of "currysetlem1" is discouraged (71 steps).
 Proof modification of "currysetlem2" is discouraged (20 steps).
 Proof modification of "currysetlem3" is discouraged (82 steps).
-Proof modification of "cygablOLD" is discouraged (379 steps).
 Proof modification of "daraptiALT" is discouraged (23 steps).
 Proof modification of "dariiALT" is discouraged (19 steps).
 Proof modification of "demoivreALT" is discouraged (1087 steps).

diff --git a/set.mm b/set.mm
@@ -32465,16 +32465,16 @@ general is seen either by substitution (when the variable ` V ` has no
     cgsex4g $p |- ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) ->
                     ( E. x E. y E. z E. w ( ch /\ ph ) <-> ps ) ) $=
       ( vv wa wex cv wceq wcel biimpa exlimivv elisset anim12i exdistrv wal weq
-      sylibr wn eqeq1 anbi1d anbi2d exbidv notbid alcomiw impbii notbii 2exnaln
-      3bitr4i exbii 4exdistrv bitri 2eximi syl biimprcd 2eximdv syl5com impbid2
-      ancld ) HLUAZIMUAZQZJLUAZKMUAZQZQZCAQZGRFRZERDRZBVSBDEVRBFGCABOUBUCUCVQCG
-      RFRZERDRZBVTVQDSHTZESZITZQZFSZJTZGSKTZQZQZGRZFRZERZDRZWBVQWFERDRZWJGRFRZQ
-      ZWOVMWPVPWQVMWCDRZWEERZQWPVKWSVLWTDHLUDEIMUDUEWCWEDEUFUIVPWHFRZWIGRZQWQVN
-      XAVOXBFJLUDGKMUDUEWHWIFGUFUIUEWOWLERFRZDRWRWNXCDWLUJZFUGEUGZUJXDEUGFUGZUJ
-      WNXCXEXFXEXFXDWFPSZJTZWIQZQZGRZUJEFPFPUHZWLXKXLWKXJGXLWJXIWFXLWHXHWIWGXGJ
-      UKULUMUNUOUPXDWCXGITZQZWJQZGRZUJFEPEPUHZWLXPXQWKXOGXQWFXNWJXQWEXMWCWDXGIU
-      KUMULUNUOUPUQURWLEFUSWLFEUSUTVAWFWJDEFGVBVCUIWMWADEWKCFGNVDVDVEBWAVSDEBCV
-      RFGBCACABOVFVJVGVGVHVI $.
+      sylibr wn eqeq1 anbi2d anbi1d exbidv notbid alcomw notbii 2exnaln 3bitr4i
+      exbii 4exdistrv bitri 2eximi syl biimprcd ancld 2eximdv syl5com impbid2 )
+      HLUAZIMUAZQZJLUAZKMUAZQZQZCAQZGRFRZERDRZBVRBDEVQBFGCABOUBUCUCVPCGRFRZERDR
+      ZBVSVPDSHTZESZITZQZFSZJTZGSKTZQZQZGRZFRZERZDRZWAVPWEERDRZWIGRFRZQZWNVLWOV
+      OWPVLWBDRZWDERZQWOVJWRVKWSDHLUDEIMUDUEWBWDDEUFUIVOWGFRZWHGRZQWPVMWTVNXAFJ
+      LUDGKMUDUEWGWHFGUFUIUEWNWKERFRZDRWQWMXBDWKUJZFUGEUGZUJXCEUGFUGZUJWMXBXDXE
+      XCWBPSZITZQZWIQZGRZUJWEXFJTZWHQZQZGRZUJEFPPEPUHZWKXJXOWJXIGXOWEXHWIXOWDXG
+      WBWCXFIUKULUMUNUOFPUHZWKXNXPWJXMGXPWIXLWEXPWGXKWHWFXFJUKUMULUNUOUPUQWKEFU
+      RWKFEURUSUTWEWIDEFGVAVBUIWLVTDEWJCFGNVCVCVDBVTVRDEBCVQFGBCACABOVEVFVGVGVH
+      VI $.
     $( $j usage 'cgsex4g' avoids 'ax-10' 'ax-11' 'ax-12'; $)
   $}
 
@@ -32506,8 +32506,15 @@ general is seen either by substitution (when the variable ` V ` has no
     ceqsex.3 $e |- ( x = A -> ( ph <-> ps ) ) $.
     $( Elimination of an existential quantifier, using implicit substitution.
        (Contributed by NM, 2-Mar-1995.)  (Revised by Mario Carneiro,
-       10-Oct-2016.) $)
+       10-Oct-2016.)  (Proof shortened by Wolf Lammen, 22-Jan-2025.) $)
     ceqsex $p |- ( E. x ( x = A /\ ph ) <-> ps ) $=
+      ( cv wceq wa wex wn wi wal alinexa nfn notbid ceqsal bitr3i con4bii ) CHD
+      IZAJCKZBUBLUAALZMCNBLZUAACOUCUDCDBCEPFUAABGQRST $.
+
+    $( Obsolete version of ~ ceqsex as of 22-Jan-2025.  (Contributed by NM,
+       2-Mar-1995.)  (Revised by Mario Carneiro, 10-Oct-2016.)
+       (New usage is discouraged.)  (Proof modification is discouraged.) $)
+    ceqsexOLD $p |- ( E. x ( x = A /\ ph ) <-> ps ) $=
       ( cv wceq wa wex biimpa exlimi wal biimprcd alrimi isseti exintr mpisyl
       wi impbii ) CHDIZAJZCKZBUCBCEUBABGLMBUBATZCNUBCKUDBUECEUBABGOPCDFQUBACRSU
       A $.
@@ -158764,22 +158771,6 @@ computer programs (as last() or lastChar()), the terminology used for
       PUKUGVFVAVSVMTVCVFVMVRUHUIUJVCVFEVOHZVAVFVFVNULHVTVCVFUMBDUNVNIVDEUOUPUQV
       GECURUS $.
 
-    $( Obsolete version of ~ ccatval1 as of 18-Jan-2024.  Value of a symbol in
-       the left half of a concatenated word.  (Contributed by Stefan O'Rear,
-       15-Aug-2015.)  (Revised by Mario Carneiro, 22-Sep-2015.)  (Proof
-       shortened by AV, 30-Apr-2020.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    ccatval1OLD $p |- ( ( S e. Word B /\ T e. Word B
-                          /\ I e. ( 0 ..^ ( # ` S ) ) )
-                     -> ( ( S ++ T ) ` I ) = ( S ` I ) ) $=
-      ( vx cword wcel cc0 chash cfv cfzo co w3a cmin cif caddc cconcat cvv wceq
-      cv cmpt ccatfval 3adant3 eleq1 fveq2 fvoveq1 ifbieq12d 3ad2ant3 sylan9eqr
-      iftrue cn0 simp3 lencl 3ad2ant2 elfzoext syl2anc fvexd fvmptd ) BAFZGZCUS
-      GZDHBIJZKLZGZMZEDETZVCGZVFBJZVFVBNLCJZOZDBJZHVBCIJZPLKLZBCQLZRUTVAVNEVMVJ
-      UASVDEBCUSUSUBUCVFDSZVEVJVDVKDVBNLCJZOZVKVOVGVDVHVIVKVPVFDVCUDVFDBUEVFDVB
-      CNUFUGVDUTVQVKSVAVDVKVPUJUHUIVEVDVLUKGZDVMGUTVAVDULVAUTVRVDACUMUNVLHVBDUO
-      UPVEDBUQUR $.
-
     $( Value of a symbol in the right half of a concatenated word.
        (Contributed by Stefan O'Rear, 15-Aug-2015.)  (Revised by Mario
        Carneiro, 22-Sep-2015.) $)
@@ -159343,15 +159334,6 @@ computer programs (as last() or lastChar()), the terminology used for
     ( cword wcel cs1 cvv cc0 chash cfv cfzo cconcat wceq s1cli ccatval1 mp3an2
     co ) DCEFAGZHEFBIDJKLRFBDSMRKBDKNAOCHDSBPQ $.
 
-  $( Obsolete version of ~ ccats1val1 as of 20-Jan-2024.  Value of a symbol in
-     the left half of a word concatenated with a single symbol.  (Contributed
-     by Alexander van der Vekens, 5-Aug-2018.)
-     (Proof modification is discouraged.)  (New usage is discouraged.) $)
-  ccats1val1OLD $p |- ( ( W e. Word V /\ S e. V /\ I e. ( 0 ..^ ( # ` W ) ) )
-                     -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) ) $=
-    ( wcel cword cs1 cc0 chash cfv cfzo cconcat wceq s1cl ccatval1OLD syl3an2
-    co ) ACEDCFZEAGZREBHDIJKQEBDSLQJBDJMACNCDSBOP $.
-
   $( Value of the symbol concatenated with a word.  (Contributed by Alexander
      van der Vekens, 5-Aug-2018.)  (Proof shortened by Alexander van der
      Vekens, 14-Oct-2018.) $)
@@ -159396,31 +159378,6 @@ computer programs (as last() or lastChar()), the terminology used for
     FULUMEOUGUHVDEVIOMBPZVIEELGOVDEVHELVLCPQUIRQUJSUTVAEUKUNVEIVAVEEEKGIVDEEKVL
     UOUPRUQRCAURUS $.
 
-  $( Obsolete version of ~ ccat2s1p1 as of 20-Jan-2024.  Extract the first of
-     two concatenated singleton words.  (Contributed by Alexander van der
-     Vekens, 22-Sep-2018.)  (Proof modification is discouraged.)
-     (New usage is discouraged.) $)
-  ccat2s1p1OLD $p |- ( ( X e. V /\ Y e. V )
-                    -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = X ) $=
-    ( wcel wa cc0 cs1 cconcat co cword chash cfzo wceq s1cl adantr adantl cn c1
-    cfv s1len a1i 1nn eqeltrdi lbfzo0 sylibr ccatval1OLD syl3anc s1fv eqtrd ) B
-    ADZCADZEZFBGZCGZHISZFUMSZBULUMAJZDZUNUQDZFFUMKSZLIDZUOUPMUJURUKBANOUKUSUJCA
-    NPUJVAUKUJUTQDVAUJUTRQUTRMUJBTUAUBUCUTUDUEOAUMUNFUFUGUJUPBMUKBAUHOUI $.
-
-  $( Obsolete version of ~ ccat2s1p2 as of 20-Jan-2024.  Extract the second of
-     two concatenated singleton words.  (Contributed by Alexander van der
-     Vekens, 22-Sep-2018.)  (Proof modification is discouraged.)
-     (New usage is discouraged.) $)
-  ccat2s1p2OLD $p |- ( ( X e. V /\ Y e. V )
-                    -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = Y ) $=
-    ( wcel c1 cs1 co chash cmin caddc cfzo wceq s1cl adantl c2 cz s1len oveq12i
-    cfv cc0 wa cconcat cword adantr clt wbr 1z 2z fzolb mpbir3an 1p1e2 eleqtrri
-    1lt2 eqtri a1i ccatval2 syl3anc oveq2i 1m1e0 fveq2d s1fv eqtrd ) BADZCADZUA
-    ZEBFZCFZUBGSZEVFHSZIGZVGSZCVEVFAUCZDZVGVLDZEVIVIVGHSZJGZKGZDZVHVKLVCVMVDBAM
-    UDVDVNVCCAMNVRVEEEOKGZVQEVSDEPDOPDEOUEUFUGUHUMEOUIUJVIEVPOKBQZVPEEJGOVIEVOE
-    JVTCQRUKUNRULUOAVFVGEUPUQVDVKCLVCVDVKTVGSCVDVJTVGVJTLVDVJEEIGTVIEEIVTURUSUN
-    UOUTCAVAVBNVB $.
-
   $( Associative law for a concatenation of a word with two singleton words.
      (Contributed by Alexander van der Vekens, 22-Sep-2018.) $)
   ccatw2s1ass $p |- ( W e. Word V -> ( ( W ++ <" X "> ) ++ <" Y "> )
@@ -245153,26 +245110,6 @@ elements of arbitrarily large orders (so ` E ` is zero) but no elements
   ${
     $d m n x y B $.  $d m x y z C $.  $d m x y z F $.  $d a b m n x y z G $.
     $d x y E $.  $d m x y H $.
-    $( Obsolete proof of ~ cygabl as of 20-Jan-2024.  A cyclic group is
-       abelian.  (Contributed by Mario Carneiro, 21-Apr-2016.)
-       (New usage is discouraged.)  (Proof modification is discouraged.) $)
-    cygablOLD $p |- ( G e. CycGrp -> G e. Abel ) $=
-      ( vy vn vx va vb vm wcel cv cfv co wceq cz wrex wa eqid eqidd simpll weq
-      wi ccyg cgrp cmg cbs wral cabl iscyg3 cplusg eqeq1 rexbidv eqeq2d cbvrexv
-      oveq1 bitrdi rspccv adantl reeanv cc zcn ad2antrl ad2antll addcomd oveq1d
-      caddc simprl simprr simplr mulgdir syl13anc 3eqtr3d oveq12 ancoms eqeq12d
-      syl5ibrcom rexlimdvva syl5bir adantr syl2and 3impib isabld r19.29an sylbi
-      ) AUAHAUBHZBIZCIZDIZAUCJZKZLZCMNZBAUDJZUEZDWKNOAUFHZDBWKWGCAWKPZWGPZUGWCW
-      LWMDWKWCWFWKHZOZWLOZEFWKAUHJZAWRWKQWRWSQWCWPWLRWREIZWKHZFIZWKHZWTXBWSKZXB
-      WTWSKZLZWRXAWTGIZWFWGKZLZGMNZXCXBWHLZCMNZXFWLXAXJTWQWJXJBWTWKBESZWJWTWHLZ
-      CMNXJXMWIXNCMWDWTWHUIUJXNXICGMCGSWHXHWTWEXGWFWGUMUKULUNUOUPWLXCXLTWQWJXLB
-      XBWKBFSWIXKCMWDXBWHUIUJUOUPWQXJXLOZXFTWLXOXIXKOZCMNGMNWQXFXIXKGCMMUQWQXPX
-      FGCMMWQXGMHZWEMHZOZOZXFXPXHWHWSKZWHXHWSKZLXTXGWEVDKZWFWGKZWEXGVDKZWFWGKZY
-      AYBXTYCYEWFWGXTXGWEXQXGURHWQXRXGUSUTXRWEURHWQXQWEUSVAVBVCXTWCXQXRWPYDYALW
-      CWPXSRZWQXQXRVEZWQXQXRVFZWCWPXSVGZWKWSWGAXGWEWFWNWOWSPZVHVIXTWCXRXQWPYFYB
-      LYGYIYHYJWKWSWGAWEXGWFWNWOYKVHVIVJXPXDYAXEYBWTXHXBWHWSVKXKXIXEYBLXBWHWTXH
-      WSVKVLVMVNVOVPVQVRVSVTWAWB $.
-
     cygctb.1 $e |- B = ( Base ` G ) $.
     $( A cyclic group is countable.  (Contributed by Mario Carneiro,
        21-Apr-2016.) $)
@@ -564551,6 +564488,31 @@ dependency is expressed in our hypothesis (called implicit
       UGCBUGCLMABCNOUCUEABUECBHAICJZUCAACBPUCUHAACBNQRSTUA $.
   $}
 
+  ${
+    $d x A $.
+    wl-ceqsal.1 $e |- F/ x ps $.
+    wl-ceqsal.2 $e |- A e. _V $.
+    wl-ceqsal.3 $e |- ( x = A -> ( ph <-> ps ) ) $.
+    $( Elimination of an existential quantifier, using implicit substitution.
+       Proving ~ ceqsal and ~ ceqsex without ~ df-clab .  (Contributed by NM,
+       2-Mar-1995.)  (Revised by Mario Carneiro, 10-Oct-2016.) $)
+    wl-ceqsex $p |- ( E. x ( x = A /\ ph ) <-> ps ) $=
+      ( cv wceq wa wex biimpa exlimi wal biimprcd alrimi isseti exintr mpisyl
+      wi impbii ) CHDIZAJZCKZBUCBCEUBABGLMBUBATZCNUBCKUDBUECEUBABGOPCDFQUBACRSU
+      A $.
+    $( $j usage 'wl-ceqsex' avoids 'df-clab'; $)
+
+    $( A representation of explicit substitution of a class for a variable,
+       inferred from an implicit substitution hypothesis.  (Contributed by NM,
+       18-Aug-1993.)  Avoid ~ df-clab .  (Revised by Wolf Lammen,
+       22-Jan-2025.) $)
+    wl-ceqsal $p |- ( A. x ( x = A -> ph ) <-> ps ) $=
+      ( cv wceq wn wi wal wa wex alinexa notnotb imbi2i albii nfn notbid
+      wl-ceqsex con2bii 3bitr4i ) CHDIZAJZJZKZCLUDUEMCNZJUDAKZCLBUDUECOUIUGCAUF
+      UDAPQRUHBUEBJCDBCESFUDABGTUAUBUC $.
+    $( $j usage 'wl-ceqsal' avoids 'df-clab'; $)
+  $}
+
   $( A specialization of ~ wl-equsal1t .  Closed form of ~ sb6rf .
      (Contributed by Wolf Lammen, 27-Jul-2019.) $)
   wl-sb6rft $p |- ( F/ x ph -> ( ph <-> A. x ( x = y -> [ x / y ] ph ) ) ) $=