ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-pre-suploc Unicode version

Axiom ax-pre-suploc 7888
Description: An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given  x  <  y, either there is an element of the set greater than  x, or  y is an upper bound.

Although this and ax-caucvg 7887 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7887.

(Contributed by Jim Kingdon, 23-Jan-2024.)

Assertion
Ref Expression
ax-pre-suploc  |-  ( ( ( A  C_  RR  /\ 
E. x  x  e.  A )  /\  ( E. x  e.  RR  A. y  e.  A  y 
<RR  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  <RR  y  ->  ( E. z  e.  A  x  <RR  z  \/  A. z  e.  A  z  <RR  y ) ) ) )  ->  E. x  e.  RR  ( A. y  e.  A  -.  x  <RR  y  /\  A. y  e.  RR  (
y  <RR  x  ->  E. z  e.  A  y  <RR  z ) ) )
Distinct variable group:    x, A, y, z

Detailed syntax breakdown of Axiom ax-pre-suploc
StepHypRef Expression
1 cA . . . . 5  class  A
2 cr 7766 . . . . 5  class  RR
31, 2wss 3121 . . . 4  wff  A  C_  RR
4 vx . . . . . . 7  setvar  x
54cv 1347 . . . . . 6  class  x
65, 1wcel 2141 . . . . 5  wff  x  e.  A
76, 4wex 1485 . . . 4  wff  E. x  x  e.  A
83, 7wa 103 . . 3  wff  ( A 
C_  RR  /\  E. x  x  e.  A )
9 vy . . . . . . . 8  setvar  y
109cv 1347 . . . . . . 7  class  y
11 cltrr 7771 . . . . . . 7  class  <RR
1210, 5, 11wbr 3987 . . . . . 6  wff  y  <RR  x
1312, 9, 1wral 2448 . . . . 5  wff  A. y  e.  A  y  <RR  x
1413, 4, 2wrex 2449 . . . 4  wff  E. x  e.  RR  A. y  e.  A  y  <RR  x
155, 10, 11wbr 3987 . . . . . . 7  wff  x  <RR  y
16 vz . . . . . . . . . . 11  setvar  z
1716cv 1347 . . . . . . . . . 10  class  z
185, 17, 11wbr 3987 . . . . . . . . 9  wff  x  <RR  z
1918, 16, 1wrex 2449 . . . . . . . 8  wff  E. z  e.  A  x  <RR  z
2017, 10, 11wbr 3987 . . . . . . . . 9  wff  z  <RR  y
2120, 16, 1wral 2448 . . . . . . . 8  wff  A. z  e.  A  z  <RR  y
2219, 21wo 703 . . . . . . 7  wff  ( E. z  e.  A  x 
<RR  z  \/  A. z  e.  A  z  <RR  y )
2315, 22wi 4 . . . . . 6  wff  ( x 
<RR  y  ->  ( E. z  e.  A  x 
<RR  z  \/  A. z  e.  A  z  <RR  y ) )
2423, 9, 2wral 2448 . . . . 5  wff  A. y  e.  RR  ( x  <RR  y  ->  ( E. z  e.  A  x  <RR  z  \/  A. z  e.  A  z  <RR  y ) )
2524, 4, 2wral 2448 . . . 4  wff  A. x  e.  RR  A. y  e.  RR  ( x  <RR  y  ->  ( E. z  e.  A  x  <RR  z  \/  A. z  e.  A  z  <RR  y ) )
2614, 25wa 103 . . 3  wff  ( E. x  e.  RR  A. y  e.  A  y  <RR  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  <RR  y  ->  ( E. z  e.  A  x  <RR  z  \/  A. z  e.  A  z  <RR  y ) ) )
278, 26wa 103 . 2  wff  ( ( A  C_  RR  /\  E. x  x  e.  A
)  /\  ( E. x  e.  RR  A. y  e.  A  y  <RR  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  <RR  y  ->  ( E. z  e.  A  x  <RR  z  \/  A. z  e.  A  z  <RR  y ) ) ) )
2815wn 3 . . . . 5  wff  -.  x  <RR  y
2928, 9, 1wral 2448 . . . 4  wff  A. y  e.  A  -.  x  <RR  y
3010, 17, 11wbr 3987 . . . . . . 7  wff  y  <RR  z
3130, 16, 1wrex 2449 . . . . . 6  wff  E. z  e.  A  y  <RR  z
3212, 31wi 4 . . . . 5  wff  ( y 
<RR  x  ->  E. z  e.  A  y  <RR  z )
3332, 9, 2wral 2448 . . . 4  wff  A. y  e.  RR  ( y  <RR  x  ->  E. z  e.  A  y  <RR  z )
3429, 33wa 103 . . 3  wff  ( A. y  e.  A  -.  x  <RR  y  /\  A. y  e.  RR  (
y  <RR  x  ->  E. z  e.  A  y  <RR  z ) )
3534, 4, 2wrex 2449 . 2  wff  E. x  e.  RR  ( A. y  e.  A  -.  x  <RR  y  /\  A. y  e.  RR  ( y  <RR  x  ->  E. z  e.  A  y  <RR  z ) )
3627, 35wi 4 1  wff  ( ( ( A  C_  RR  /\ 
E. x  x  e.  A )  /\  ( E. x  e.  RR  A. y  e.  A  y 
<RR  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  <RR  y  ->  ( E. z  e.  A  x  <RR  z  \/  A. z  e.  A  z  <RR  y ) ) ) )  ->  E. x  e.  RR  ( A. y  e.  A  -.  x  <RR  y  /\  A. y  e.  RR  (
y  <RR  x  ->  E. z  e.  A  y  <RR  z ) ) )
Colors of variables: wff set class
This axiom is referenced by:  axsuploc  7985
  Copyright terms: Public domain W3C validator