save ax-riotaBAD in glbconN

add discouraged tags to direct consequences of ax-riotaBAD 1218 -> 1154 (-64) dependents on ax-riotaBAD no $j usage since ax-riotaBAD will be deleted extra: 'autominimize' subsym1 (it would be automatic but nsb was changed to closed form; no tag or old)
metamath · Jan 3, 2025 · 046a140 · 046a140
1 parent 5afff8a
commit 046a140
Show file tree

Hide file tree

Showing 2 changed files with 90 additions and 14 deletions.
diff --git a/discouraged b/discouraged
@@ -1450,6 +1450,7 @@
 "ax-pre-lttrn" is used by "axlttrn".
 "ax-pre-mulgt0" is used by "axmulgt0".
 "ax-pre-sup" is used by "axsup".
+"ax-riotaBAD" is used by "riotaclbgBAD".
 "ax10fromc7" is used by "axc5c711".
 "ax10fromc7" is used by "equidq".
 "ax10fromc7" is used by "hba1-o".
@@ -5138,7 +5139,6 @@
 "dfsb1" is used by "bj-dfsb2".
 "dfsb1" is used by "drsb1".
 "dfsb1" is used by "frege55b".
-"dfsb1" is used by "subsym1".
 "dfsb2" is used by "dfsb3".
 "dfvd1imp" is used by "gen11".
 "dfvd1impr" is used by "gen11".
@@ -12596,7 +12596,31 @@
 "ringcvalALTV" is used by "ringcbasALTV".
 "ringcvalALTV" is used by "ringccofvalALTV".
 "ringcvalALTV" is used by "ringchomfvalALTV".
+"riotaclbBAD" is used by "cdlemk36".
+"riotaclbBAD" is used by "glbconNOLD".
+"riotaclbgBAD" is used by "riotaclbBAD".
+"riotaclbgBAD" is used by "riotasvd".
 "riotaocN" is used by "glbconN".
+"riotaocN" is used by "glbconNOLD".
+"riotasv" is used by "cdleme26e".
+"riotasv" is used by "cdleme26eALTN".
+"riotasv" is used by "cdleme26f".
+"riotasv" is used by "cdleme26f2".
+"riotasv" is used by "cdleme26f2ALTN".
+"riotasv" is used by "cdleme26fALTN".
+"riotasv2d" is used by "cdleme42b".
+"riotasv2d" is used by "riotasv2s".
+"riotasv3d" is used by "cdleme40m".
+"riotasv3d" is used by "cdleme40n".
+"riotasv3d" is used by "cdleme41sn3a".
+"riotasv3d" is used by "cdleme43fsv1snlem".
+"riotasv3d" is used by "cdlemefs32sn1aw".
+"riotasv3d" is used by "cdlemkid".
+"riotasv3d" is used by "dihvalcqpre".
+"riotasvd" is used by "cdleme32a".
+"riotasvd" is used by "riotasv".
+"riotasvd" is used by "riotasv2d".
+"riotasvd" is used by "riotasv3d".
 "rnbra" is used by "bra11".
 "rnbra" is used by "cnvbraval".
 "rnelshi" is used by "hmopidmchi".
@@ -14646,6 +14670,7 @@ New usage of "ax-pre-lttri" is discouraged (1 uses).
 New usage of "ax-pre-lttrn" is discouraged (1 uses).
 New usage of "ax-pre-mulgt0" is discouraged (1 uses).
 New usage of "ax-pre-sup" is discouraged (1 uses).
+New usage of "ax-riotaBAD" is discouraged (1 uses).
 New usage of "ax1" is discouraged (0 uses).
 New usage of "ax10fromc7" is discouraged (3 uses).
 New usage of "ax10w" is discouraged (0 uses).
@@ -16052,7 +16077,7 @@ New usage of "dfnul3OLD" is discouraged (0 uses).
 New usage of "dfnul4OLD" is discouraged (0 uses).
 New usage of "dfpjop" is discouraged (4 uses).
 New usage of "dfrecs3OLD" is discouraged (0 uses).
-New usage of "dfsb1" is discouraged (4 uses).
+New usage of "dfsb1" is discouraged (3 uses).
 New usage of "dfsb2" is discouraged (1 uses).
 New usage of "dfsb3" is discouraged (0 uses).
 New usage of "dfsn2ALT" is discouraged (0 uses).
@@ -16773,6 +16798,7 @@ New usage of "gidsn" is discouraged (1 uses).
 New usage of "gidval" is discouraged (3 uses).
 New usage of "glb0N" is discouraged (2 uses).
 New usage of "glbconN" is discouraged (1 uses).
+New usage of "glbconNOLD" is discouraged (0 uses).
 New usage of "glbconxN" is discouraged (1 uses).
 New usage of "goeqi" is discouraged (0 uses).
 New usage of "golem1" is discouraged (1 uses).
@@ -18855,7 +18881,14 @@ New usage of "ringcinvALTV" is discouraged (1 uses).
 New usage of "ringcisoALTV" is discouraged (0 uses).
 New usage of "ringcsectALTV" is discouraged (1 uses).
 New usage of "ringcvalALTV" is discouraged (3 uses).
-New usage of "riotaocN" is discouraged (1 uses).
+New usage of "riotaclbBAD" is discouraged (2 uses).
+New usage of "riotaclbgBAD" is discouraged (2 uses).
+New usage of "riotaocN" is discouraged (2 uses).
+New usage of "riotasv" is discouraged (6 uses).
+New usage of "riotasv2d" is discouraged (2 uses).
+New usage of "riotasv2s" is discouraged (0 uses).
+New usage of "riotasv3d" is discouraged (7 uses).
+New usage of "riotasvd" is discouraged (4 uses).
 New usage of "rlimaddOLD" is discouraged (0 uses).
 New usage of "rlimmulOLD" is discouraged (0 uses).
 New usage of "rmoanimALT" is discouraged (0 uses).
@@ -20700,6 +20733,7 @@ Proof modification of "ggen22" is discouraged (13 steps).
 Proof modification of "ggen31" is discouraged (22 steps).
 Proof modification of "ghomidOLD" is discouraged (178 steps).
 Proof modification of "ghomlinOLD" is discouraged (161 steps).
+Proof modification of "glbconNOLD" is discouraged (904 steps).
 Proof modification of "grpbaseOLD" is discouraged (11 steps).
 Proof modification of "grpinvfvalALT" is discouraged (161 steps).
 Proof modification of "grposnOLD" is discouraged (291 steps).

diff --git a/set.mm b/set.mm
@@ -547923,8 +547923,7 @@ A Fne if ( S = (/) , { X } , U. S ) ) $=
      See ~ negsym1 for more information.  (Contributed by Anthony Hart,
      11-Sep-2011.) $)
   subsym1 $p |- ( [ y / x ] [ y / x ] F. -> [ y / x ] ph ) $=
-    ( wfal wsb weq wi wa wex fal intnan nex dfsb1 mtbir pm2.21i ) DBCEZBCEZABCE
-    QBCFZPGZRPHZBIZHUASTBPRPRDGZRDHZBIZHUDUBUCBDRJKLKDBCMNKLKPBCMNO $.
+    ( wfal wsb wn nsb fal mpg pm2.21i ) DBCEZBCEZABCEKFZLFBKBCGDFMBDBCGHIIJ $.
 
 $( (End of Anthony Hart's mathbox.) $)
 $( End $[ set-mbox-ah.mm $] $)
@@ -587194,14 +587193,14 @@ This axiom is _logically_ redundant in the (logically complete)
      Mario Carneiro, 15-Oct-2016.)  WARNING:  THIS "AXIOM", WHICH IS THE OLD
      ~ df-riota , CONFLICTS WITH (THE NEW) ~ df-riota AND MAKES THE SYSTEM IN
      set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES
-     ARE ELIMINATED. $)
+     ARE ELIMINATED. (New usage is discouraged.) $)
   ax-riotaBAD $a |- ( iota_ x e. A ph ) = if ( E! x e. A ph ,
     ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) ) $.
 
   ${
     $d x A $.
     $( Closure of restricted iota.  (Contributed by NM, 28-Feb-2013.)  (Revised
-       by Mario Carneiro, 24-Dec-2016.) $)
+       by Mario Carneiro, 24-Dec-2016.)  (New usage is discouraged.) $)
     riotaclbgBAD $p |- ( A e. V
           -> ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) ) $=
       ( wcel wreu crio riotacl wn cund cfv undefnel2 cv cio cab cif ax-riotaBAD
@@ -587210,7 +587209,8 @@ This axiom is _logically_ redundant in the (logically complete)
       ZUOBOZJKZPURUJUMUIUPURSABCQCUQJBCTUAUBUCUDUEUFUG $.
 
     riotaclb.1 $e |- A e. _V $.
-    $( Closure of restricted iota.  (Contributed by NM, 15-Sep-2011.) $)
+    $( Closure of restricted iota.  (Contributed by NM, 15-Sep-2011.)
+       (New usage is discouraged.) $)
     riotaclbBAD $p |- ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) $=
       ( cvv wcel wreu crio wb riotaclbgBAD ax-mp ) CEFABCGABCHCFIDABCEJK $.
   $}
@@ -587222,7 +587222,8 @@ This axiom is _logically_ redundant in the (logically complete)
         -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) ) $.
     riotasvd.2 $e |- ( ph -> D e. A ) $.
     $( Deduction version of ~ riotasv .  (Contributed by NM, 4-Mar-2013.)
-       (Revised by Mario Carneiro, 15-Oct-2016.) $)
+       (Revised by Mario Carneiro, 15-Oct-2016.)
+       (New usage is discouraged.) $)
     riotasvd $p |- ( ( ph /\ A e. V ) -> ( ( y e. B /\ ps ) -> D = C ) ) $=
       ( vz wcel wa cv wceq wi wral adantr syl crio wsbc wreu eqeltrrd wb adantl
       riotaclbgBAD mpbird riotasbc eqeq1 imbi2d ralbidv nfra1 nfcv nfeq2 ralbid
@@ -587247,7 +587248,7 @@ This axiom is _logically_ redundant in the (logically complete)
     riotasv2d.9 $e |- ( ph -> ch ) $.
     $( Value of description binder ` D ` for a single-valued class expression
        ` C ( y ) ` (as in e.g. ~ reusv2 ).  Special case of ~ riota2f .
-       (Contributed by NM, 2-Mar-2013.) $)
+       (Contributed by NM, 2-Mar-2013.)  (New usage is discouraged.) $)
     riotasv2d $p |- ( ( ph /\ A e. V ) -> D = F ) $=
       ( wcel cvv wceq elex wa adantr cv wi eleq1 adantl anbi12d imbi12d adantlr
       wb eqeq2d riotasvd nfv nfan nfcvd nfvd nfand wnfc wral crio nfra1 nfriota
@@ -587264,7 +587265,8 @@ This axiom is _logically_ redundant in the (logically complete)
     $( The value of description binder ` D ` for a single-valued class
        expression ` C ( y ) ` (as in e.g. ~ reusv2 ) in the form of a
        substitution instance.  Special case of ~ riota2f .  (Contributed by NM,
-       3-Mar-2013.)  (Proof shortened by Mario Carneiro, 6-Dec-2016.) $)
+       3-Mar-2013.)  (Proof shortened by Mario Carneiro, 6-Dec-2016.)
+       (New usage is discouraged.) $)
     riotasv2s $p |- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) )
             -> D = [_ E / y ]_ C ) $=
       ( wcel wsbc wa w3a csb wceq cv nfan a1i adantl 3simpc simp1 wi wral nfra1
@@ -587282,7 +587284,7 @@ This axiom is _logically_ redundant in the (logically complete)
     $( Value of description binder ` D ` for a single-valued class expression
        ` C ( y ) ` (as in e.g. ~ reusv2 ).  Special case of ~ riota2f .
        (Contributed by NM, 26-Jan-2013.)  (Proof shortened by Mario Carneiro,
-       6-Dec-2016.) $)
+       6-Dec-2016.)  (New usage is discouraged.) $)
     riotasv $p |- ( ( D e. A /\ y e. B /\ ph ) -> D = C ) $=
       ( wcel cv wceq cvv wa wi wral crio a1i id riotasvd mpan2 3impib ) GDJZCKE
       JZAGFLZUCDMJUDANUEOHUCABCDEFGMGABKFLOCEPBDQLUCIRUCSTUAUB $.
@@ -587302,7 +587304,7 @@ This axiom is _logically_ redundant in the (logically complete)
        expression ` C ( y ) ` (see e.g. ~ reusv2 ) also holds for its
        description binder ` D ` (in the form of property ` th ` ).
        (Contributed by NM, 5-Mar-2013.)  (Revised by Mario Carneiro,
-       15-Oct-2016.) $)
+       15-Oct-2016.)  (New usage is discouraged.) $)
     riotasv3d $p |- ( ( ph /\ A e. V ) -> th ) $=
       ( wcel wa cvv elex wrex adantr wi wral nfv imp adantrl wceq riotasvd impr
       cv wb eqcomd syldan mpbid exp45 ralrimd wnf r19.23t syl sylibd mpd sylan2
@@ -594199,11 +594201,51 @@ X C ( ._|_ ` Y ) ) ) $=
     glbcon.o $e |- ._|_ = ( oc ` K ) $.
     $( De Morgan's law for GLB and LUB. This holds in any complete
        ortholattice, although we assume ` HL ` for convenience.  (Contributed
-       by NM, 17-Jan-2012.)  (New usage is discouraged.) $)
+       by NM, 17-Jan-2012.)  New ~ df-riota .  (Revised by SN, 3-Jan-2025.)
+       (New usage is discouraged.) $)
     glbconN $p |- ( ( K e. HL /\ S C_ B )
         -> ( G ` S ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) ) $=
       ( vz vu wcel cfv wceq wbr wral wi wa vy vw vv vt wss chlt cv crab sseqin2
       cin biimpi dfin5 eqtr3di fveq2d cple crio eqid biid id ssrab2 glbval cops
+      a1i wreu hlop ccla cdm hlclat clatglbcl2 syl2anc glbeu breq1 breq2 imbi2d
+      ralbidv anbi12d riotaocN ad2antrr opoccl sylancom wrex opococ rspceeqv wb
+      eqcomd fveq2 eleq1 imbi12d adantl ralxfrd simpr simplr oplecon3b ralbidva
+      syl3anc bitr4d ralrab weq eleq1d 3bitr4g ad3antrrr riotabidva simpl mpan2
+      lubval eqtr4d 3eqtrd sylan9eqr ) CBUEZFUFNZCEOAUGZCNZABUHZEOZXKGOZCNZABUH
+      ZDOZGOZXICXMEXIBCUJZCXMXIXTCPCBUIUKABCULUMUNXJXNUAUGZLUGZFUOOZQZLXMRZUBUG
+      ZYBYCQZLXMRZYFYAYCQZSZUBBRZTZUABUPZUCUGZGOZYBYCQZLXMRZYHYFYOYCQZSZUBBRZTZ
+      UCBUPZGOZXSXJYLUALUBBXMEFYCUFHYCUQZJYLURZXJUSZXMBUEZXJXLABUTVCZVAXJFVBNZY
+      LUABVDYMUUCPFVEZXJYLUALUBBXMEFYCUFHUUDJUUEUUFXJFVFNUUGXMEVGNFVHUUHBXMEFHJ
+      VIVJVKYLUUAUAUCBFGHKYAYOPZYEYQYKYTUUKYDYPLXMYAYOYBYCVLVOUUKYJYSUBBUUKYIYR
+      YHYAYOYFYCVMVNVOVPVQVJXJUUBXRGXJUUBMUGZYNYCQZMXQRZUULUDUGZYCQZMXQRZYNUUOY
+      CQZSZUDBRZTZUCBUPZXRXJUUAUVAUCBXJYNBNZTZYQUUNYTUUTUVDYBCNZYPSZLBRZUULGOZC
+      NZUUMSZMBRZYQUUNUVDUVGUVIYOUVHYCQZSZMBRUVKUVDUVFUVMLMUVHBBUVDUULBNZUUIUVH
+      BNZXJUUIUVCUVNUUJVRZBFGUULHKVSZVTUVDYBBNZTZYBGOZBNZYBUVTGOZPZYBUVHPZMBWAZ
+      UVDUVRUUIUWAXJUUIUVCUVRUUJVRZBFGYBHKVSZVTUVSUWBYBUVDUVRUUIUWBYBPZUWFBFGYB
+      HKWBZVTWEMUVTBUVHUWBYBUULUVTGWFWCZVJUWDUVFUVMWDUVDUWDUVEUVIYPUVLYBUVHCWGZ
+      YBUVHYOYCVMWHWIWJUVDUVJUVMMBUVDUVNTZUUMUVLUVIUWLUUIUVNUVCUUMUVLWDUVPUVDUV
+      NWKXJUVCUVNWLBFYCGUULYNHUUDKWMWOVNWNWPXLUVEYPLABXKYBCWGZWQXPUVIUUMMABAMWR
+      XOUVHCXKUULGWFWSZWQWTUVDYTUUOGOZYBYCQZLXMRZUWOYOYCQZSZUDBRUUTUVDYSUWSUBUD
+      UWOBBUVDUUOBNZUUIUWOBNXJUUIUVCUWTUUJVRZBFGUUOHKVSVTUVDYFBNZTZYFGOZBNZYFUX
+      DGOZPYFUWOPZUDBWAUVDUXBUUIUXEXJUUIUVCUXBUUJVRZBFGYFHKVSVTUXCUXFYFUVDUXBUU
+      IUXFYFPUXHBFGYFHKWBVTWEUDUXDBUWOUXFYFUUOUXDGWFWCVJUXGYSUWSWDUVDUXGYHUWQYR
+      UWRUXGYGUWPLXMYFUWOYBYCVLVOYFUWOYOYCVLWHWIWJUVDUUSUWSUDBUVDUWTTZUUQUWQUUR
+      UWRUXIUVIUUPSZMBRZUVEUWPSZLBRZUUQUWQUXIUXKUVIUWOUVHYCQZSZMBRUXMUXIUXJUXOM
+      BUXIUVNTZUUPUXNUVIUXPUUIUVNUWTUUPUXNWDXJUUIUVCUWTUVNUUJXAZUXIUVNWKUVDUWTU
+      VNWLBFYCGUULUUOHUUDKWMWOVNWNUXIUXLUXOLMUVHBBUXIUVNUUIUVOUXQUVQVTUXIUVRTZU
+      WAUWCUWEUXIUVRUUIUWAXJUUIUVCUWTUVRUUJXAZUWGVTUXRUWBYBUXIUVRUUIUWHUXSUWIVT
+      WEUWJVJUWDUXLUXOWDUXIUWDUVEUVIUWPUXNUWKYBUVHUWOYCVMWHWIWJWPXPUVIUUPMABUWN
+      WQXLUVEUWPLABUWMWQWTUXIUUIUVCUWTUURUWRWDUXAXJUVCUWTWLUVDUWTWKBFYCGYNUUOHU
+      UDKWMWOWHWNWPVPXBXJXQBUEZXRUVBPXPABUTXJUXTTUVAUCMUDBXQDFYCUFHUUDIUVAURXJU
+      XTXCXJUXTWKXEXDXFUNXGXH $.
+
+    $( Obsolete version of ~ glbconN as of 3-Jan-2025.  (Contributed by NM,
+       17-Jan-2012.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    glbconNOLD $p |- ( ( K e. HL /\ S C_ B )
+        -> ( G ` S ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) ) $=
+      ( vz vu wcel cfv wceq wbr wral wi wa vy vw vv vt wss chlt cv crab sseqin2
+      cin biimpi dfin5 eqtr3di fveq2d cple crio eqid biid id ssrab2 glbval cops
       wreu hlop ccla hlclat clatglbcl sylancl eqeltrrd fvexi riotaclbBAD sylibr
       a1i breq1 ralbidv breq2 imbi2d anbi12d riotaocN syl2anc ad2antrr sylancom
       cbs opoccl wrex opococ eqcomd fveq2 rspceeqv eleq1 imbi12d adantl ralxfrd