Add axsuploc to iset.mm

This is similar to axsup in set.mm but is for ax-pre-suploc instead of
ax-pre-sup .  The proof is based on ltxrlt .

iset.mm

@@ -82474,6 +82474,33 @@ product of extended reals (common case).  (Contributed by David A.
     mpan remulcl sylancr 3imtr4d ) ACDZBCDZEZFAGHZFBGHZEFABIJZGHZFAKHZFBKHZEFUF
     KHZABLUAUHUDUBUIUEFCDZUAUHUDMNFAOQUKUBUIUEMNFBOQPUCUKUFCDUJUGMNABRFUFOST $.
 
+  ${
+    $d x y z A $.
+    $( An inhabited, bounded-above, located set of reals has a supremum.  Axiom
+       for real and complex numbers, derived from ZF set theory.  (This
+       restates ~ ax-pre-suploc with ordering on the extended reals.)
+       (Contributed by Jim Kingdon, 30-Jan-2024.) $)
+    axsuploc $p |- ( ( ( A C_ RR /\ E. x x e. A )
+        /\ ( E. x e. RR A. y e. A y < x
+        /\ A. x e. RR A. y e. RR ( x < y
+          -> ( E. z e. A x < z \/ A. z e. A z < y ) ) ) )
+        -> E. x e. RR ( A. y e. A -. x < y /\
+          A. y e. RR ( y < x -> E. z e. A y < z ) ) ) $=
+      ( cr cv wcel wa clt wral wrex wi cltrr wb ltxrlt ralbidva rexbidva simplr
+      wbr syl2anc wss wex wo wn ssel2 sylan an32s simpr simpllr adantlr orbi12d
+      imbi12d anbi12d adantr pm5.32i ax-pre-suploc sylbi bicomd notbid ad2antrr
+      mpbid ) DEUAZAFZDGAUBZHZBFZVCISZBDJZAEKZVCVFISZVCCFZISZCDKZVKVFISZCDJZUCZ
+      LZBEJZAEJZHZHZVCVFMSZUDZBDJZVFVCMSZVFVKMSZCDKZLZBEJZHZAEKZVJUDZBDJZVGVFVK
+      ISZCDKZLZBEJZHZAEKZWAVEWEBDJZAEKZWBVCVKMSZCDKZVKVFMSZCDJZUCZLZBEJZAEJZHZH
+      WKVEVTXJVBVTXJNVDVBVIXAVSXIVBVHWTAEVBVCEGZHZVGWEBDVBVFDGZXKVGWENZVBXMHVFE
+      GZXKXNDEVFUEZVFVCOZUFUGPQVBVRXHAEXLVQXGBEXLXOHZVJWBVPXFXRXKXOVJWBNZVBXKXO
+      RZXLXOUHZVCVFOZTXRVMXCVOXEXRVLXBCDXRVKDGZHZXKVKEGZVLXBNVBXKXOYCUIXLYCYEXO
+      VBYCYEXKDEVKUEUJUJZVCVKOTQXRVNXDCDYDYEXOVNXDNYFXLXOYCRZVKVFOTPUKULPPUMUNU
+      OABCDUPUQVBWKWSNVDVTVBWJWRAEXLWDWMWIWQXLWCWLBDXLXMHZWBVJYHVJWBYHXKXOXSVBX
+      KXMRVBXMXOXKXPUJYBTURUSPXLWHWPBEXRWEVGWGWOXRVGWEXRXOXKXNYAXTXQTURXRWFWNCD
+      YDWNWFYDXOYEWNWFNYGYFVFVKOTURQULPUMQUTVA $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

mmil.raw.html

@@ -5587,7 +5587,7 @@
 
 <TR>
 <TD>axsup</TD>
-<TD>~ ax-pre-suploc , ~ caucvgre</TD>
+<TD>~ axsuploc</TD>
 </TR>
 
 <TR>