save ax-riotaBAD in glbconN

discouraged

@@ -5138,7 +5138,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".
@@ -12597,6 +12596,7 @@
 "ringcvalALTV" is used by "ringccofvalALTV".
 "ringcvalALTV" is used by "ringchomfvalALTV".
 "riotaocN" is used by "glbconN".
+"riotaocN" is used by "glbconNOLD".
 "rnbra" is used by "bra11".
 "rnbra" is used by "cnvbraval".
 "rnelshi" is used by "hmopidmchi".
@@ -16052,7 +16052,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 +16773,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 +18856,7 @@ 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 "riotaocN" is discouraged (2 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 +20701,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).

set.mm

@@ -547914,17 +547914,14 @@ A Fne if ( S = (/) , { X } , U. S ) ) $=
      See ~ negsym1 for more information.  (Contributed by Anthony Hart,
      13-Sep-2011.) $)
   amosym1 $p |- ( E* x E* x F. -> E* x ph ) $=
-    ( wfal wmo wex weu wi moeu wn mofal 19.8a notnotd ax-mp pm2.21i notnoti nex
-    eunex mto ja sylbi ) CBDZBDUABEZUABFZGABDZUABHUBUCUDUBIZUDUAUEIBJZUAUBUABKL
-    MNUCUDUCUAIZBEUGBUAUFOPUABQRNST $.
+    ( wfal wmo mofal a1i moimi ) ACBDZBHABEFG $.
 
   $( A symmetry with ` [ x / y ] ` .
 
      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 sbv falim sylbi sbimi ) DBCEZABCJDADBCFAGHI $.
 
 $( (End of Anthony Hart's mathbox.) $)
 $( End $[ set-mbox-ah.mm $] $)
@@ -594199,11 +594196,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