set2.mm-base

GinoGiotto · Aug 10, 2023 · a9d3676 · a9d3676
1 parent 03be88d
commit a9d3676
Showing 1 changed file with 33 additions and 24 deletions.
diff --git a/set.mm b/set.mm
@@ -21576,7 +21576,8 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
     $( Equivalence for substitution.  (Contributed by NM, 2-Jun-1993.)  (Proof
        shortened by Wolf Lammen, 23-Sep-2018.) $)
     sb6a $p |- ( [ y / x ] ph <-> A. x ( x = y -> [ x / y ] ph ) ) $=
-      ( wsb weq wi wal sbco sb6 bitr3i ) ABCDACBDZBCDBCEKFBGABCHKBCIJ $.
+      ( wsb weq wi wal sbcom3vv sb6 sbid sbbii 3bitr3ri ) ACBDZBCDACCDZBCDBCEMF
+      BGABCDACBCHMBCINABCACJKL $.
   $}
 
   ${
@@ -23008,17 +23009,18 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
     2mo $p |- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <->
               A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) ->
                                                       ( x = z /\ y = w ) ) ) $=
-      ( weq wa wi wal wex wsb wmo nfmo1 nfe1 nfmo nfan 19.8a spsbe sbimi nfv wn
-      2mo2 biimpi 19.21bbi syl2ani sbcom2 sylbi anim12ii alrimi alrimivv sylbir
-      nfs1v nfsb pm3.21 imim1d alimd com12 aleximi 2nexaln 2sb8e xchnxbi pm2.21
-      mo3 2alimi 2eximi 19.23bi pm2.61d1 impbii alrot4 bitri ) ABDFZCEFZGZHZCIZ
-      BIZEJZDJZAACEKZBDKZGZVMHZCIZBIZEIZDIZWBEIDICIBIVRWFVRACJZBLZABJZCLZGZWFAB
-      CDEUBWKWDDEWKWCBWHWJBWGBMWIBCABNOPWKWBCWHWJCWGCBACNOWICMPWHWAVKWJVLAWHWGW
-      GBDKZVKVTACQVSWGBDACERSWHWGWLGVKHZBDWHWMDIBIWGBDWGDTVCUCUDUEAWJWIWICEKZVL
-      VTABQVTABDKZCEKWNACEBDUFWOWICEABDRSUGWJWIWNGVLHZCEWJWPEICIWICEWIETVCUCUDU
-      EUHUIUIUJUKWFVTEJZDJZVRWEWQVQDWDVTVPEVTWDVPVTWCVOBVSBDULVTWBVNCVSBDCACEUL
-      UMVTAWAVMVTAUNUOUPUPUQURURWRUAAUAZCIBIZVRWGBJWTWRABCUSABCDEUTVAWTVREWTEJV
-      RDWTVPDEWSVNBCAVMVBVDVEVFVFUGVGVHWBDEBCVIVJ $.
+      ( weq wa wi wal wex wsb wmo nfmo1 wnf wtru nftru nfe1 a1i nfmodv nfv 2mo2
+      mptru 19.8a spsbe sbimi mo3 biimpi 19.21bbi syl2ani sbcom2 sylbi anim12ii
+      nfan alrimi alrimivv sylbir nfs1v nfsbv pm3.21 imim1d alimd com12 aleximi
+      2nexaln 2sb8ev xchnxbi pm2.21 2alimi 2eximi 19.23bi pm2.61d1 impbii bitri
+      wn alrot4 ) ABDFZCEFZGZHZCIZBIZEJZDJZAACEKZBDKZGZVRHZCIZBIZEIZDIZWGEIDICI
+      BIWCWKWCACJZBLZABJZCLZGZWKABCDEUAWPWIDEWPWHBWMWOBWLBMWOBNOWNBCCPWNBNOABQR
+      SUBUMWPWGCWMWOCWMCNOWLCBBPWLCNOACQRSUBWNCMUMWMWFVPWOVQAWMWLWLBDKZVPWEACUC
+      WDWLBDACEUDUEWMWLWQGVPHZBDWMWRDIBIWLBDWLDTUFUGUHUIAWOWNWNCEKZVQWEABUCWEAB
+      DKZCEKWSACEBDUJWTWNCEABDUDUEUKWOWNWSGVQHZCEWOXAEICIWNCEWNETUFUGUHUIULUNUN
+      UOUPWKWEEJZDJZWCWJXBWBDWIWEWAEWEWIWAWEWHVTBWDBDUQWEWGVSCWDBDCACEUQURWEAWF
+      VRWEAUSUTVAVAVBVCVCXCVNAVNZCIBIZWCWLBJXEXCABCVDABCDEAETADTVEVFXEWCEXEEJWC
+      DXEWADEXDVSBCAVRVGVHVIVJVJUKVKVLWGDEBCVOVM $.
   $}
 
   ${
@@ -29213,12 +29215,16 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
        version without disjoint variable condition on ` x , y ` .  (Contributed
        by NM, 13-Oct-1999.)  (Revised by Mario Carneiro, 14-Oct-2016.) $)
     ralcom $p |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph ) $=
-      ( nfcv ralcomf ) ABCDECDFBEFG $.
+      ( cv wcel wa wi wal wral ancomst 2albii alcom bitri r2al 3bitr4i ) BFDGZC
+      FEGZHAIZCJBJZSRHAIZBJCJZACEKBDKABDKCEKUAUBCJBJUCTUBBCRSALMUBBCNOABCDEPACB
+      EDPQ $.
 
     $( Commutation of restricted existential quantifiers.  (Contributed by NM,
        19-Nov-1995.)  (Revised by Mario Carneiro, 14-Oct-2016.) $)
     rexcom $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $=
-      ( nfcv rexcomf ) ABCDECDFBEFG $.
+      ( cv wcel wa wex wrex ancom anbi1i 2exbii excom bitri r2ex 3bitr4i ) BFDG
+      ZCFEGZHZAHZCIBIZSRHZAHZBICIZACEJBDJABDJCEJUBUDCIBIUEUAUDBCTUCARSKLMUDBCNO
+      ABCDEPACBEDPQ $.
   $}
 
   ${
@@ -29934,9 +29940,10 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
        quantifier with implicit substitution which also changes the quantifier
        domain.  Deduction form.  (Contributed by David Moews, 1-May-2017.) $)
     cbvraldva2 $p |- ( ph -> ( A. x e. A ps <-> A. y e. B ch ) ) $=
-      ( cv wcel wi wal wral weq wa simpr eleq12d imbi12d df-ral cbvaldva
-      3bitr4g ) ADJZFKZBLZDMEJZGKZCLZEMBDFNCEGNAUEUHDEADEOZPZUDUGBCUJUCUFFGAUIQ
-      IRHSUABDFTCEGTUB $.
+      ( cv wcel wi wal wral weq wb wa simpr 19.21v df-ral eleq12d pm5.74ri
+      imbi12d expcom pm5.74d cbvalvw 3bitr3i 3bitr4g ) ADJZFKZBLZDMZEJZGKZCLZEM
+      ZBDFNCEGNAULUPAUKLZDMAUOLZEMAULLAUPLUQURDEDEOZAUKUOAUSUKUOPAUSQZUJUNBCUTU
+      IUMFGAUSRIUAHUCUDUEUFAUKDSAUOESUGUBBDFTCEGTUH $.
 
     $( Rule used to change the bound variable in a restricted existential
        quantifier with implicit substitution which also changes the quantifier
@@ -31688,7 +31695,8 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
        (Contributed by NM, 13-Sep-1999.) $)
     rspc2v $p |- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ph ->
                   ps ) ) $=
-      ( nfv rspc2 ) ABCDEFGHICDLBELJKM $.
+      ( wcel wral cv wceq ralbidv rspcv sylan9 ) FHLAEIMZDHMCEIMZGILBSTDFHDNFOA
+      CEIJPQCBEGIKQR $.
 
     $( 2-variable restricted specialization, using implicit substitution.
        (Contributed by NM, 18-Jun-2014.) $)
@@ -38895,7 +38903,9 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
     $( Rearrange restricted quantifiers.  (Contributed by NM, 11-Mar-1997.) $)
     raaanv $p |- ( A. x e. A A. y e. A ( ph /\ ps ) <->
                   ( A. x e. A ph /\ A. y e. A ps ) ) $=
-      ( nfv raaan ) ABCDEADFBCFG $.
+      ( wa wral wb wceq rzal pm5.1 syl12anc wne r19.28zv ralbidv r19.27zv bitrd
+      c0 pm2.61ine ) ABFDEGZCEGZACEGZBDEGZFZHZERERIUAUBUCUETCEJACEJBDEJUAUDKLER
+      MZUAAUCFZCEGUDUFTUGCEABDENOAUCCEPQS $.
   $}
 
   ${
@@ -38904,8 +38914,7 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
        (Contributed by Rodolfo Medina, 7-Jul-2010.)  (Proof shortened by Mario
        Carneiro, 14-Nov-2016.) $)
     sbss $p |- ( [ y / x ] x C_ A <-> y C_ A ) $=
-      ( vz cv wss wsb vex sbequ sseq1 nfv sbie vtoclb ) AEZCFZADGDEZCFZOABGBEZC
-      FDRBHODBAIPRCJOQADQAKNPCJLM $.
+      ( vz cv wss sseq1 sbievw2 ) AEZCFBEZCFDEZCFABDIKCGKJCGH $.
   $}
 
   ${
@@ -50242,9 +50251,9 @@ Contrast with domain (defined in ~ df-dm ).  For alternate definitions,
        28-Dec-2014.) $)
     sosn $p |- ( Rel R -> ( R Or { A } <-> -. A R A ) ) $=
       ( vx vy csn wor wpo wrel wbr wn cv weq wral wcel wa elsni eqcomd sylan9eq
-      w3o 3mix2d rgen2a df-so mpbiran2 posn syl5bb ) AEZBFZUFBGZBHAABIJUGUHCKZD
-      KZBIZCDLZUJUIBIZSZDUFMCUFMUNCDUFUIUFNZUJUFNZOULUKUMUOUPUIAUJUIAPUPUJAUJAP
-      QRTUACDUFBUBUCABUDUE $.
+      w3o 3mix2d rgen2 df-so mpbiran2 posn syl5bb ) AEZBFZUFBGZBHAABIJUGUHCKZDK
+      ZBIZCDLZUJUIBIZSZDUFMCUFMUNCDUFUFUIUFNZUJUFNZOULUKUMUOUPUIAUJUIAPUPUJAUJA
+      PQRTUACDUFBUBUCABUDUE $.
 
     $( Founded relation on a singleton.  (Contributed by Mario Carneiro,
        28-Dec-2014.)  (Revised by Mario Carneiro, 23-Apr-2015.) $)