mathbox: global minimization

discouraged

@@ -18179,6 +18179,7 @@ Proof modification of "bj-sb56" is discouraged (50 steps).
 Proof modification of "bj-sbceqgALT" is discouraged (143 steps).
 Proof modification of "bj-sbeqALT" is discouraged (44 steps).
 Proof modification of "bj-sbidmOLD" is discouraged (41 steps).
+Proof modification of "bj-sbievv" is discouraged (25 steps).
 Proof modification of "bj-spcimdv" is discouraged (56 steps).
 Proof modification of "bj-spcimdvv" is discouraged (56 steps).
 Proof modification of "bj-spimtv" is discouraged (52 steps).

set.mm

@@ -530926,11 +530926,10 @@ proof is intuitionistic (use of ~ ax-3 comes from the unusual definition
        (Revised by BJ, 26-Dec-2023.) $)
     bj-ififc $p |-
                  ( X e. if ( ph , A , B ) <-> if- ( ph , X e. A , X e. B ) ) $=
-      ( vx cif wcel cv wif cab bj-df-ifc eleq2i cvv elex wa wn wo df-ifp adantl
-      eleq1 jaoi sylbi wceq biidd ifpbi123d elabg pm5.21nii bitri ) DABCFZGDAEH
-      ZBGZUJCGZIZEJZGZADBGZDCGZIZUIUNDAEBCKLUODMGZURDUNNURAUPOZAPZUQOZQUSAUPUQR
-      UTUSVBUPUSADBNSUQUSVADCNSUAUBUMUREDMUJDUCZAUKULAUPUQVCAUDUJDBTUJDCTUEUFUG
-      UH $.
+      ( vx cif wcel cv wif cab bj-df-ifc eleq2i wa wn wo cvv df-ifp elex adantl
+      eleq1 jaoi sylbi wceq biidd ifpbi123d elab3 bitri ) DABCFZGDAEHZBGZUICGZI
+      ZEJZGADBGZDCGZIZUHUMDAEBCKLULUPEDUPAUNMZANZUOMZODPGZAUNUOQUQUTUSUNUTADBRS
+      UOUTURDCRSUAUBUIDUCZAUJUKAUNUOVAAUDUIDBTUIDCTUEUFUG $.
   $}
 
 
@@ -531358,7 +531357,7 @@ Utility lemmas or strengthenings of theorems in the main part (biconditional
   $( Closed form of ~ 2exbii .  (Contributed by BJ, 6-May-2019.) $)
   bj-2exbi $p |- ( A. x A. y ( ph <-> ps ) ->
                                          ( E. x E. y ph <-> E. x E. y ps ) ) $=
-    ( wb wal wex exbi alimi syl ) ABEDFZCFADGZBDGZEZCFLCGMCGEKNCABDHILMCHJ $.
+    ( wb wal wex exbi alexbii ) ABEDFADGBDGCABDHI $.
 
   $( Closed form of ~ 3exbii .  (Contributed by BJ, 6-May-2019.) $)
   bj-3exbi $p |- ( A. x A. y A. z ( ph <-> ps ) ->
@@ -532297,7 +532296,7 @@ standard proof of the implication in modal logic (B5 ` => ` 4).  Its dual
      nonfreeness implies the "exists" form of nonfreeness.  (Contributed by BJ,
      9-Dec-2023.) $)
   bj-wnfenf $p |- ( ( E. x ph -> A. x ps ) -> A. x ( E. x ph -> ps ) ) $=
-    ( wex wal wi bj-wnf1 sp imim2i sylg ) ACDZBCEZFZMKBFCABCGLBKBCHIJ $.
+    ( wex wal wi bj-wnf1 bj-19.21bit sylg ) ACDZBCEFZKJBFCABCGJBCHI $.
 
 
 $(
@@ -532585,8 +532584,8 @@ quantifiers appear (since they typically require ~ ax-10 to work with),
      this could also be proved from ~ bj-nnfim , ~ bj-nnfe1 and ~ bj-nnfa1 .
      (Contributed by BJ, 9-Dec-2023.) $)
   bj-wnfnf $p |- F// x ( E. x ph -> A. x ps ) $=
-    ( wex wal wi wnnf wa bj-wnf2 bj-wnf1 pm3.2i df-bj-nnf mpbir ) ACDBCEFZCGNCD
-    NFZNNCEFZHOPABCIABCJKNCLM $.
+    ( wex wal wi wnnf bj-wnf2 bj-wnf1 df-bj-nnf mpbir2an ) ACDBCEFZCGLCDLFLLCEF
+    ABCHABCILCJK $.
 
   $( A variable is nonfree in a formula if and only if it is nonfree in its
      negation.  The foward implication is intuitionistically valid (and that
@@ -533638,7 +533637,8 @@ References are made to the second edition (1927, reprinted 1963) of
     bj-sbievv.nfy $e |- F/ y ph $.
     bj-sbievv.is $e |- ( x = y -> ( ph <-> ps ) ) $.
     $( Version of ~ sbie with a second nonfreeness hypothesis and shorter
-       proof.  (Contributed by BJ, 18-Jul-2023.) $)
+       proof.  (Contributed by BJ, 18-Jul-2023.)
+       (Proof modification is discouraged.) $)
     bj-sbievv $p |- ( [ y / x ] ph <-> ps ) $=
       ( wsb weq wi wal sb6f equsal bitri ) ACDHCDIAJCKBACDFLABCDEGMN $.
   $}
@@ -535026,20 +535026,20 @@ FOL part ( ~ bj-ru0 ) and then two versions ( ~ bj-ru1 and ~ bj-ru ).
        application of ~ ax-rep .  (Contributed by BJ, 6-Oct-2018.) $)
     bj-snsetex $p |- ( A e. V -> { x | { x } e. A } e. _V ) $=
       ( vy vz vt vu wcel cv csn cvv wex wi wceq syl wal wb wa wsb bitri elisset
-      cab eleq2 abbidv eleq1 biimpd eximi 19.35 biimpi com12 ax-rep 19.3v sbbii
-      csb wsbc sbsbc sbceq2g elv bj-csbsn eqeq2i eqtr2 vex sylan2b syl2anb gen2
-      sneqr nfa1 mo mpg bj-sbel1 eleq1i df-clab anbi2i eleq1a eqcoms imdistanri
-      mpbir impac impbii exbii snex isseti 19.42v mpbiran2 3bitr4ri bibi2i mpbi
-      albii dfcleq issetri ax5e ) BCHZAIJZBHZAUBZKHZDLZWPWLWMDIZHZAUBZKHZWPMZDL
-      ZWQWLWRBNZDLXCDBCUAXDXBDXDWTWONZXBXDWSWNAWRBWMUCUDXEXAWPWTWOKUEUFOUGOXAXC
-      WQMDXCXADPZWQXCXFWQMXAWPDUHUIUJEWTEIZWTNZELFIZXGHZXIWTHZQZFPZELZXJGIZWRHZ
-      XOXIJZNZEPZRZGLZQZFPZELZXNXSXIXGNZMFPELZYDGXRDEFGUKYFXSXSFESZRYEMZEPFPYHF
-      EXSXRXRFESZYEYGXREULZXSXRFEYJUMYIXRXOXGJZNZYEYIXOFXGXQUNZNZYLYIXRFXGUOZYN
-      XRFEUPYOYNQEFXGXOXQKUQURTYMYKXOFXGUSUTTXRYLRXQYKNYEXOXQYKVAXIXGFVBVFOVCVD
-      VEXSFEXREVGVHVQVIYCXMEYBXLFYAXKXJWSAFSZXQWRHZXKYAYPAXIWMUNZWRHYQAFWMWRVJY
-      RXQWRAXIUSVKTWSFAVLYAYQXRRZGLZYQXTYSGXTXPXRRZYSXSXRXPYJVMUUAYSXRXPYQXPYQM
-      XQXOXPXQXONYQXOWRXQVNUJVOVPYQXRXPXQWRXOVNVRVSTVTYTYQXRGLGXQXIWAWBYQXRGWCW
-      DTWEWFWHVTWGXHXMEFXGWTWIVTVQWJVIOWPDWKO $.
+      cab eleq2 abbidv eleq1 biimpd eximi bj-eximcom com12 19.3v sbbii csb wsbc
+      ax-rep sbsbc sbceq2g elv bj-csbsn eqeq2i eqtr2 sneqr sylan2b syl2anb gen2
+      vex nfa1 mo mpbir bj-sbel1 eleq1i df-clab anbi2i eleq1a eqcoms imdistanri
+      impac impbii exbii snex isseti 19.42v mpbiran2 3bitr4ri bibi2i albii mpbi
+      mpg dfcleq issetri ax5e ) BCHZAIJZBHZAUBZKHZDLZWOWKWLDIZHZAUBZKHZWOMZDLZW
+      PWKWQBNZDLXBDBCUAXCXADXCWSWNNZXAXCWRWMAWQBWLUCUDXDWTWOWSWNKUEUFOUGOWTXBWP
+      MDXBWTDPWPWTWODUHUIEWSEIZWSNZELFIZXEHZXGWSHZQZFPZELZXHGIZWQHZXMXGJZNZEPZR
+      ZGLZQZFPZELZXLXQXGXENZMFPELZYBGXPDEFGUNYDXQXQFESZRYCMZEPFPYFFEXQXPXPFESZY
+      CYEXPEUJZXQXPFEYHUKYGXPXMXEJZNZYCYGXMFXEXOULZNZYJYGXPFXEUMZYLXPFEUOYMYLQE
+      FXEXMXOKUPUQTYKYIXMFXEURUSTXPYJRXOYINYCXMXOYIUTXGXEFVEVAOVBVCVDXQFEXPEVFV
+      GVHWGYAXKEXTXJFXSXIXHWRAFSZXOWQHZXIXSYNAXGWLULZWQHYOAFWLWQVIYPXOWQAXGURVJ
+      TWRFAVKXSYOXPRZGLZYOXRYQGXRXNXPRZYQXQXPXNYHVLYSYQXPXNYOXNYOMXOXMXNXOXMNYO
+      XMWQXOVMUIVNVOYOXPXNXOWQXMVMVPVQTVRYRYOXPGLGXOXGVSVTYOXPGWAWBTWCWDWEVRWFX
+      FXKEFXEWSWHVRVHWIWGOWODWJO $.
   $}
 
   ${
@@ -535506,9 +535506,9 @@ the projections (see ~ df-bj-pr1 and ~ df-bj-pr2 ).  (Contributed by BJ,
   bj-pr22val $p |- pr2 (| A ,, B |) = B $=
     ( bj-c2uple bj-cpr2 bj-c1upl c1o csn bj-ctag cxp cun c0 df-bj-2upl bj-pr2eq
     wceq ax-mp bj-pr2un eqtri cif bj-pr2val 3eqtri df-bj-1upl 1n0 iffalsei eqid
-    nesymi iftruei uneq12i uncom un0 ) ABCZDZAEZDZFGBHIZDZJZKBJZBUKULUNJZDZUPUJ
-    URNUKUSNABLUJURMOULUNPQUMKUOBUMKGAHIZDZKFNZAKRKULUTNUMVANAUAULUTMOKASVBAKFK
-    UBUEUCTUOFFNZBKRBFBSVCBKFUDUFQUGUQBKJBKBUHBUIQT $.
+    nesymi iftruei uneq12i 0un ) ABCZDZAEZDZFGBHIZDZJZKBJBUJUKUMJZDZUOUIUPNUJUQ
+    NABLUIUPMOUKUMPQULKUNBULKGAHIZDZKFNZAKRKUKURNULUSNAUAUKURMOKASUTAKFKUBUEUCT
+    UNFFNZBKRBFBSVABKFUDUFQUGBUHT $.
 
   $( Sethood of the second projection.  (Contributed by BJ, 6-Oct-2018.) $)
   bj-pr2ex $p |- ( A e. V -> pr2 A e. _V ) $=
@@ -535548,14 +535548,14 @@ sethood hypotheses (compare ~ opth ).  (Contributed by BJ, 6-Oct-2018.) $)
      values of n.  (Contributed by BJ, 21-Apr-2019.) $)
   bj-2upln1upl $p |- (| A ,, B |) =/= (| C |) $=
     ( bj-c1upl cdif wne wpss c1o csn bj-ctag cxp cun wss difeq2i cin wceq ax-mp
-    c0 mpbi 0pss bj-c2uple xpundi bj-disjsn01 xpdisj1 eqtr3i disjdif2 1oex snnz
-    incom wa bj-tagn0 pm3.2i xpnz eqnetri eqnetrri mpbir ssun2 sscon df-bj-2upl
-    ssdif sstri df-bj-1upl uneq1i eqtri difeq1i sseqtrri psssstr mp2an difn0 )
-    ABUAZCDZEZRFZVJVKFRVLGZVMRHIZBJZKZRIZAJZKZVRCJZKZLZEZGZWDVLMVNWEWDRFVQVRVSW
-    ALZKZEZWDRWGWCVQVRVSWAUBNWHVQRVQWGOZRPWHVQPWGVQOZWIRWGVQUIVRVOORPWJRPUCVRVO
-    WFVPUDQUEVQWGUFQVORFZVPRFZUJVQRFWKWLHUGUHBUKULVOVPUMSUNUOWDTUPWDVJWBEZVLWDV
-    TVQLZWBEZWMWDVQWBEZWOWBWCMWDWPMWBVTUQWBWCVQURQVQWNMWPWOMVQVTUQVQWNWBUTQVAVJ
-    WNWBVJADZVQLWNABUSWQVTVQAVBVCVDVEVFVKWBVJCVBNVFRWDVLVGVHVLTSVJVKVIQ $.
+    c0 mpbi 0pss bj-c2uple xpundi incom xp01disjl eqtr3i disjdif2 1oex bj-tagn0
+    wa snnz xpnz eqnetri eqnetrri mpbir ssun2 sscon ssdif df-bj-2upl df-bj-1upl
+    pm3.2i sstri uneq1i eqtri difeq1i sseqtrri psssstr mp2an difn0 ) ABUAZCDZEZ
+    RFZVIVJFRVKGZVLRHIZBJZKZRIZAJZKZVQCJZKZLZEZGZWCVKMVMWDWCRFVPVQVRVTLZKZEZWCR
+    WFWBVPVQVRVTUBNWGVPRVPWFOZRPWGVPPWFVPOWHRWFVPUCWEVOUDUEVPWFUFQVNRFZVORFZUIV
+    PRFWIWJHUGUJBUHUTVNVOUKSULUMWCTUNWCVIWAEZVKWCVSVPLZWAEZWKWCVPWAEZWMWAWBMWCW
+    NMWAVSUOWAWBVPUPQVPWLMWNWMMVPVSUOVPWLWAUQQVAVIWLWAVIADZVPLWLABURWOVSVPAUSVB
+    VCVDVEVJWAVICUSNVERWCVKVFVGVKTSVIVJVHQ $.
 
 
 $(
@@ -535797,8 +535797,8 @@ sethood hypotheses (compare ~ opth ).  (Contributed by BJ, 6-Oct-2018.) $)
      related by the membership relation (i.e., the first is an element of the
      second) and the second is a set (hence so is the first).  TODO: move to
      Main after reordering to have ~ brrelex2i available.  Check if it is
-     shorter to prove ~ bj-epelg first or ~ bj-epelb first. (Contributed by BJ,
-     14-Jul-2023.) $)
+     shorter to prove ~ bj-epelg first or ~ bj-epelb first.  (Contributed by
+     BJ, 14-Jul-2023.) $)
   bj-epelb $p |- ( A _E B <-> ( A e. B /\ B e. _V ) ) $=
     ( cep wbr cvv wcel wa rele brrelex2i pm4.71i epelg pm5.32ri bitri ) ABCDZNB
     EFZGABFZOGNOABCHIJONPABEKLM $.
@@ -535982,8 +535982,8 @@ Moore collections ( ~ df-mre ), topologies ( ~ df-top ), pi-systems, rings of
      ~ bj-restsnss2 .  TODO: this is ~ restsn .  (Contributed by BJ,
      27-Apr-2021.) $)
   bj-restsn0 $p |- ( A e. V -> ( { (/) } |`t A ) = { (/) } ) $=
-    ( wcel c0 wss wa csn crest co wceq 0ss jctr bj-restsnss2 syl ) ABCZODAEZFDG
-    ZAHIQJOPAKLABDMN $.
+    ( wcel c0 wss csn crest co wceq 0ss bj-restsnss2 mpan2 ) ABCDAEDFZAGHMIAJAB
+    DKL $.
 
   $( Special case of ~ bj-restsn , ~ bj-restsnss , and ~ bj-rest10 .
      (Contributed by BJ, 27-Apr-2021.) $)
@@ -536108,18 +536108,17 @@ Moore collections ( ~ df-mre ), topologies ( ~ df-top ), pi-systems, rings of
        ~ restuni and ~ restuni2 .  (Contributed by BJ, 27-Apr-2021.) $)
     bj-restuni $p |-
              ( ( X e. V /\ A e. W ) -> U. ( X |`t A ) = ( U. X i^i A ) ) $=
-      ( vx vy vz wcel wa cuni cin cv wex eluni bicomi anbi1i 19.42v bitri exbii
-      3bitri crest co wceq wrex elrest anbi2d exbidv wb a1i df-rex anbi2i excom
-      an12 eqimss sseld imdistanri eqimss2 impbii vex inex1 isseti biantru elin
-      biid bianass ancom 19.41v 3bitr4g bitrd syl5bb eqrdv ) DBHACHIZEDAUAUBZJZ
-      DJZAKZELZVNHVQFLZHZVRVMHZIZFMZVLVQVPHZFVQVMNVLWBVSVRGLZAKZUCZGDUDZIZFMZWC
-      VLWAWHFVLVTWGVSGVRADBCUEUFUGVLVQWDHZWDDHZIZGMZVQAHZIZVQVOHZWNIZWIWCWOWQUH
-      VLWMWPWNWPWMGVQDNOPUIWIVSWKWFIZIZGMZFMWSFMZGMZWOWHWTFWHVSWRGMZIZWTWGXCVSW
-      FGDUJUKWTXDVSWRGQORSWSFGULXBWLWNIZGMWOXAXEGXAWKVSWFIZIZFMWKXFFMZIZXEWSXGF
-      VSWKWFUMSWKXFFQXIWKWJWNIZIWKWJIZWNIXEXHXJWKXHVQWEHZWFIZFMXLWFFMZIZXJXFXMF
-      XFXMWFVSXLWFVRWEVQVRWEUNUOUPWFXLVSWFWEVRVQWEVRUQUOUPURSXLWFFQXOXLXJXLXOXN
-      XLFWEWDAGUSUTVAVBOVQWDAVCRTUKXJWJWNWKXJVDVEXKWLWNWKWJVFPTTSWLWNGVGRTVQVOA
-      VCVHVIVJVK $.
+      ( vx vy vz wcel wa cuni cin cv wex eluni bicomi 19.42v bitri exbii 3bitri
+      sseld crest co wceq wrex elrest anbi2d exbidv wb anbi1i a1i df-rex anbi2i
+      excom an12 eqimss imdistanri eqimss2 impbii vex inex1 isseti biantru elin
+      bianassc 19.41v 3bitr4g bitrd syl5bb eqrdv ) DBHACHIZEDAUAUBZJZDJZAKZELZV
+      LHVOFLZHZVPVKHZIZFMZVJVOVNHZFVOVKNVJVTVQVPGLZAKZUCZGDUDZIZFMZWAVJVSWFFVJV
+      RWEVQGVPADBCUEUFUGVJVOWBHZWBDHZIZGMZVOAHZIZVOVMHZWLIZWGWAWMWOUHVJWKWNWLWN
+      WKGVODNOUIUJWGVQWIWDIZIZGMZFMWQFMZGMZWMWFWRFWFVQWPGMZIZWRWEXAVQWDGDUKULWR
+      XBVQWPGPOQRWQFGUMWTWJWLIZGMWMWSXCGWSWIVQWDIZIZFMWIXDFMZIXCWQXEFVQWIWDUNRW
+      IXDFPXFWHWLWIXFVOWCHZWDIZFMXGWDFMZIZWHWLIZXDXHFXDXHWDVQXGWDVPWCVOVPWCUOTU
+      PWDXGVQWDWCVPVOWCVPUQTUPURRXGWDFPXJXGXKXGXJXIXGFWCWBAGUSUTVAVBOVOWBAVCQSV
+      DSRWJWLGVEQSVOVMAVCVFVGVHVI $.
   $}
 
   $( The union of an elementwise intersection on a family of sets by a subset
@@ -536869,9 +536868,8 @@ is a Moore collection ( ~ bj-snmoore ), this can also be stated as
     bj-brab2a1.2 $e |- R = { <. x , y >. | ph } $.
     $( "Unbounded" version of ~ brab2a .  (Contributed by BJ, 25-Dec-2023.) $)
     bj-brab2a1 $p |- ( A R B <-> ( ( A e. _V /\ B e. _V ) /\ ps ) ) $=
-      ( wbr cvv wcel wa biid copab cv vex pm3.2i biantrur opabbii eqtri brab2a
-      bitri ) EFGJZUDEKLFKLMBMUDNABCDEFKKGHGACDOCPKLZDPKLZMZAMZCDOIAUHCDUGAUEUF
-      CQDQRSTUAUBUC $.
+      ( cvv copab cv wcel wa vex pm3.2i biantrur opabbii eqtri brab2a ) ABCDEFJ
+      JGHGACDKCLJMZDLJMZNZANZCDKIAUDCDUCAUAUBCODOPQRST $.
   $}
 
 
@@ -536937,7 +536935,7 @@ both are sets (all three classes are equal, so they all belong to ` V ` ,
   $( If the intersection of two classes is a set, then these classes are equal
      if and only if one is an element of the singleton formed on the other.
      Stronger form of ~ elsng and ~ elsn2g (which could be proved from it).
-     (Contributed by BJ, 20-Jan-2024.). $)
+     (Contributed by BJ, 20-Jan-2024.).  (Contributed by BJ, 20-Jan-2024.) $)
   bj-elsn0 $p |- ( ( A i^i B ) e. V -> ( A e. { B } <-> A = B ) ) $=
     ( cin wcel csn wceq elsni wi wa cvv bj-inexeqex simpl elsng biimprd 3syl ex
     pm2.43d impbid2 ) ABDCEZABFEZABGZABHTUBUATUBUBUAIZTUBJAKEZBKEZJUDUCABCLUDUE
@@ -537115,15 +537113,15 @@ both are sets (all three classes are equal, so they all belong to ` V ` ,
      (Contributed by BJ, 22-Jun-2019.) $)
   bj-elid6 $p |- ( B e. ( _I |` A ) <->
                           ( B e. ( A X. A ) /\ ( 1st ` B ) = ( 2nd ` B ) ) ) $=
-    ( cid cres wcel cvv cxp wa c1st cfv c2nd wceq df-res elin2 1st2nd2 wb eleq1
-    adantl opelxp bitri biancomi bj-elid4 pm5.32i cop pm4.71ri simpl a1i syl5ib
-    jcad elex anim2i impbid1 adantr 3bitr4g bicomd 3bitrd pm5.32da simpr impbii
-    wi ancri syl6bb syl5bb pm5.32ri ) BCADZEZBAFGZEZBCEZHZBAAGZEZBIJZBKJZLZHZVF
-    VHVIBCVGVECAMNUAVJVHVOHVPVHVIVOBAFUBUCVOVHVLVHBVMVNUDZLZVHHZVOVLVHVRBAFOUEV
-    OVSVRVLHZVLVOVRVHVLVOVRHZVHVQVGEZVQVKEZVLVRVHWBPVOBVQVGQRWAVMAEZVNFEZHZWDVN
-    AEZHZWBWCVOWFWHPVRVOWFWHVOWFWDWGWFWDUTVOWDWEUFZUGWFWDVOWGWIVMVNAQUHUIWGWEWD
-    VNAUJUKULUMVMVNAFSVMVNAASUNVRWCVLPVOVRVLWCBVQVKQUORUPUQVTVLVRVLURVLVRBAAOVA
-    USVBVCVDTT $.
+    ( cid cres wcel cvv cxp wa c1st cfv c2nd wceq df-res elin2 biancomi 1st2nd2
+    wb eleq1 adantl opelxp bj-elid4 pm5.32i cop pm4.71ri wi simpl a1i jcad elex
+    syl5ib anim2i impbid1 adantr bicomd 3bitrd simpr ancri impbii syl6bb syl5bb
+    3bitr4g pm5.32da pm5.32ri 3bitri ) BCADZEZBAFGZEZBCEZHVHBIJZBKJZLZHBAAGZEZV
+    LHVFVHVIBCVGVECAMNOVHVIVLBAFUAUBVLVHVNVHBVJVKUCZLZVHHZVLVNVHVPBAFPUDVLVQVPV
+    NHZVNVLVPVHVNVLVPHZVHVOVGEZVOVMEZVNVPVHVTQVLBVOVGRSVSVJAEZVKFEZHZWBVKAEZHZV
+    TWAVLWDWFQVPVLWDWFVLWDWBWEWDWBUEVLWBWCUFZUGWDWBVLWEWGVJVKARUJUHWEWCWBVKAUIU
+    KULUMVJVKAFTVJVKAATVAVPWAVNQVLVPVNWABVOVMRUNSUOVBVRVNVPVNUPVNVPBAAPUQURUSUT
+    VCVD $.
 
   $( Characterization of the elements of the diagonal of a Cartesian square.
      (Contributed by BJ, 22-Jun-2019.) $)
@@ -538243,39 +538241,39 @@ singleton on a couple (with disjoint domain) at a point in the domain
                                    ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) ) $=
       ( vt cfv c1 cv wceq wa wcel cfn adantr vx vy vz cfinsum co cop wf1o chash
       cfz cplusg cn cmpt cseq wex cn0 wrex cio df-ov c2nd cdm c1st cbs wf copab
-      ccmn cvv df-bj-finsum a1i wb simpr fveq2d fex syl2anc op1stg eqtrd op2ndg
-      wi dmeqd fdmd f1oeq3 biimpd ad2antll adantrd eqidd simprl adantrr simprrl
-      fveq1d mpteq2dva seqeq123d simprr jca hashfz1 eqcomd ad2antrl fzfid 19.8a
+      cvv df-bj-finsum wb wi simpr fveq2d fex syl2anc op1stg eqtrd op2ndg dmeqd
+      ccmn fdmd f1oeq3 biimpd ad2antll adantrd simprl adantrr simprrl mpteq2dva
+      eqidd fveq1d seqeq123d simprr anim1ci hashfz1 eqcomd ad2antrl fzfid 19.8a
       hasheqf1oi sylc 3eqtrd sylan2 fveq12d eqeq2d impancom com12 biimprd simpl
       jcad tru jctir syl adantlrr impcom syl12anc impbid ex imp exbidv rexbidva
       wtru iotabidv eleq1 feq2 anbi12d ceqsexgv mpbir2and exsimpr df-rex sylibr
-      fveq2 feq3d rexbidv feq1 anbi2d opelopabg iotaex fvmptd syl5eq ) ABCUDUEB
-      CUFZUDMNEOZUIUEZGDOZUGZHOZGUHMZBUJMZFUKFOZUUBMZCMZULZNUMZMZPZQZDUNZEUOUPZ
-      HUQZBCUDURAUAYSUUAUAOZUSMZUTZUUBUGZUUDYTUURVAMZUJMZFUKUUHUUSMZULZNUMZMZPZ
-      QZDUNZEUOUPZHUQZUUQUBOZVERZLOZUVMVBMZUCOZVCZLSUPZQZUBUCVDZUDVFUDUAUWAUVLU
-      LPAUAUBUCLDEFHVGVHAUURYSPZQZUVKUUPHUWCUVJUUOEUOUWCYTUORZQUVIUUNDUWCUWDUVI
-      UUNVIZUWCUVBBPZUUSCPZUUTGPZUWDUWEVQUWCUVBYSVAMZBUWCUURYSVAAUWBVJZVKUWCBVE
-      RZCVFRZUWIBPAUWKUWBITZAUWLUWBAGBVBMZCVCZGSRZUWLKJGUWNSCVLVMZTZBCVEVFVNVMV
-      OUWCUUSYSUSMZCUWCUURYSUSUWJVKUWCUWKUWLUWSCPUWMUWRBCVEVFVPVMVOZUWCUUTCUTZG
-      UWCUUSCUWTVRAUXAGPUWBAGUWNCKVSTVOUWFUWGUWHQZQZUWDUWEUXCUWDQZUVIUUNUXDUVIU
-      UCUUMUXCUVIUUCVQUWDUXCUVAUUCUVHUWHUVAUUCVQUWFUWGUWHUVAUUCUUTGUUAUUBVTZWAW
-      BWCTUVIUXDUUMUVAUXDUVHUUMUVAUXDQZUVHUUMUXFUVGUULUUDUXFYTUUEUVFUUKUXFUVCUU
-      FUVEUUJNNUXFNWDUVAUXCUVCUUFPUWDUVAUXCQZUVBBUJUVAUWFUXBWEVKWFUVAUXCUVEUUJP
-      UWDUXGFUKUVDUUIUXGUUGUKRZQUUHUUSCUXGUWGUXHUVAUWFUWGUWHWGTWHWIWFWJUXDUVAUW
-      DUWHQZYTUUEPZUXDUWDUWHUXCUWDVJUXCUWHUWDUWFUWGUWHWKZTWLUVAUXIQZYTUUAUHMZUU
-      TUHMZUUEUWDYTUXMPUVAUWHUWDUXMYTYTWMWNWOUXLUUASRUVADUNZUXMUXNPUXLNYTWPUVAU
-      XOUXIUVADWQTUUAUUTDSWRWSUXLUUTGUHUVAUWDUWHWKVKWTZXAXBXCWAXDXEXHUXDUUNUVAU
-      VHUXDUUCUVAUUMUXCUUCUVAVQZUWDUWHUXQUWFUWGUWHUVAUUCUXEXFWBTZWCUUNUXDUVHUUC
-      UXDUUMUVHUUCUXDQZUUMUVHUXSUULUVGUUDUXSUUEYTUUKUVFUXSUUFUVCUUJUVENNUXSNWDU
-      XSBUVBUJUXSUWFXTQZBUVBPUXCUXTUUCUWDUXCUWFXTUWFUXBXGXIXJWOUXTUVBBUWFXTXGWN
-      XKVKUXSFUKUUIUVDUUCUXCUXHUUIUVDPUWDUUCUXCQZUXHQUUHCUUSUYACUUSPZUXHUXBUYBU
-      UCUWFUXBUUSCUWGUWHXGWNWBTWHXLWIWJUXSYTUUEUXSUVAUWDUWHUXJUXDUUCUVAUXRXMUUC
-      UXCUWDWKUXCUWHUUCUWDUXKWOUXPXNWNXBXCWAXDXEXHXOXPXNXQXRXSYAAYSUWARZUWKUVOU
-      WNCVCZLSUPZIAUVOSRZUYDQZLUNZUYEAUVOGPZUYGQLUNZUYHAUYJUWPUWOJKAUWPUYJUWPUW
-      OQZVIJUYGUYKLGSUYIUYFUWPUYDUWOUVOGSYBUVOGUWNCYCYDYEXKYFUYIUYGLYGXKUYDLSYH
-      YIAUWKUWLUYCUWKUYEQZVIIUWQUVTUWKUVOUWNUVQVCZLSUPZQUYLUBUCBCVEVFUVMBPZUVNU
-      WKUVSUYNUVMBVEYBUYOUVRUYMLSUYOUVPUWNUVQUVOUVMBVBYJYKYLYDUVQCPZUYNUYEUWKUY
-      PUYMUYDLSUVOUWNUVQCYMYLYNYOVMYFUUQVFRAUUPHYPVHYQYR $.
+      fveq2 feq3d rexbidv feq1 anbi2d opelopabg iotaex a1i fvmptd2 syl5eq ) ABC
+      UDUEBCUFZUDMNEOZUIUEZGDOZUGZHOZGUHMZBUJMZFUKFOZUUBMZCMZULZNUMZMZPZQZDUNZE
+      UOUPZHUQZBCUDURAUAYSUUAUAOZUSMZUTZUUBUGZUUDYTUURVAMZUJMZFUKUUHUUSMZULZNUM
+      ZMZPZQZDUNZEUOUPZHUQUUQUBOZVQRZLOZUVLVBMZUCOZVCZLSUPZQZUBUCVDZUDVEUAUBUCL
+      DEFHVFAUURYSPZQZUVKUUPHUWBUVJUUOEUOUWBYTUORZQUVIUUNDUWBUWCUVIUUNVGZUWBUVB
+      BPZUUSCPZUUTGPZUWCUWDVHUWBUVBYSVAMZBUWBUURYSVAAUWAVIZVJUWBBVQRZCVERZUWHBP
+      AUWJUWAITZAUWKUWAAGBVBMZCVCZGSRZUWKKJGUWMSCVKVLZTZBCVQVEVMVLVNUWBUUSYSUSM
+      ZCUWBUURYSUSUWIVJUWBUWJUWKUWRCPUWLUWQBCVQVEVOVLVNZUWBUUTCUTZGUWBUUSCUWSVP
+      AUWTGPUWAAGUWMCKVRTVNUWEUWFUWGQZQZUWCUWDUXBUWCQZUVIUUNUXCUVIUUCUUMUXBUVIU
+      UCVHUWCUXBUVAUUCUVHUWGUVAUUCVHUWEUWFUWGUVAUUCUUTGUUAUUBVSZVTWAWBTUVIUXCUU
+      MUVAUXCUVHUUMUVAUXCQZUVHUUMUXEUVGUULUUDUXEYTUUEUVFUUKUXEUVCUUFUVEUUJNNUXE
+      NWGUVAUXBUVCUUFPUWCUVAUXBQZUVBBUJUVAUWEUXAWCVJWDUVAUXBUVEUUJPUWCUXFFUKUVD
+      UUIUXFUUGUKRZQUUHUUSCUXFUWFUXGUVAUWEUWFUWGWETWHWFWDWIUXCUVAUWCUWGQZYTUUEP
+      ZUXBUWGUWCUWEUWFUWGWJZWKUVAUXHQZYTUUAUHMZUUTUHMZUUEUWCYTUXLPUVAUWGUWCUXLY
+      TYTWLWMWNUXKUUASRUVADUNZUXLUXMPUXKNYTWOUVAUXNUXHUVADWPTUUAUUTDSWQWRUXKUUT
+      GUHUVAUWCUWGWJVJWSZWTXAXBVTXCXDXGUXCUUNUVAUVHUXCUUCUVAUUMUXBUUCUVAVHZUWCU
+      WGUXPUWEUWFUWGUVAUUCUXDXEWATZWBUUNUXCUVHUUCUXCUUMUVHUUCUXCQZUUMUVHUXRUULU
+      VGUUDUXRUUEYTUUKUVFUXRUUFUVCUUJUVENNUXRNWGUXRBUVBUJUXRUWEXSQZBUVBPUXBUXSU
+      UCUWCUXBUWEXSUWEUXAXFXHXIWNUXSUVBBUWEXSXFWMXJVJUXRFUKUUIUVDUUCUXBUXGUUIUV
+      DPUWCUUCUXBQZUXGQUUHCUUSUXTCUUSPZUXGUXAUYAUUCUWEUXAUUSCUWFUWGXFWMWATWHXKW
+      FWIUXRYTUUEUXRUVAUWCUWGUXIUXCUUCUVAUXQXLUUCUXBUWCWJUXBUWGUUCUWCUXJWNUXOXM
+      WMXAXBVTXCXDXGXNXOXMXPXQXRXTAYSUVTRZUWJUVNUWMCVCZLSUPZIAUVNSRZUYCQZLUNZUY
+      DAUVNGPZUYFQLUNZUYGAUYIUWOUWNJKAUWOUYIUWOUWNQZVGJUYFUYJLGSUYHUYEUWOUYCUWN
+      UVNGSYAUVNGUWMCYBYCYDXJYEUYHUYFLYFXJUYCLSYGYHAUWJUWKUYBUWJUYDQZVGIUWPUVSU
+      WJUVNUWMUVPVCZLSUPZQUYKUBUCBCVQVEUVLBPZUVMUWJUVRUYMUVLBVQYAUYNUVQUYLLSUYN
+      UVOUWMUVPUVNUVLBVBYIYJYKYCUVPCPZUYMUYDUWJUYOUYLUYCLSUVNUWMUVPCYLYKYMYNVLY
+      EUUQVERAUUPHYOYPYQYR $.
 
 $(
   @( Value of a finite sum.  (Contributed by BJ, 9-Jun-2019.) @)