Metamath Proof Explorer


Axiom ax-pre-sup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup . Note: Normally new proofs would use axsup . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-sup
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y  E. x e. RR ( A. y e. A -. x  E. z e. A y 

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cr
 |-  RR
2 0 1 wss
 |-  A C_ RR
3 c0
 |-  (/)
4 0 3 wne
 |-  A =/= (/)
5 vx
 |-  x
6 vy
 |-  y
7 6 cv
 |-  y
8 cltrr
 |-  
9 5 cv
 |-  x
10 7 9 8 wbr
 |-  y 
11 10 6 0 wral
 |-  A. y e. A y 
12 11 5 1 wrex
 |-  E. x e. RR A. y e. A y 
13 2 4 12 w3a
 |-  ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y 
14 9 7 8 wbr
 |-  x 
15 14 wn
 |-  -. x 
16 15 6 0 wral
 |-  A. y e. A -. x 
17 vz
 |-  z
18 17 cv
 |-  z
19 7 18 8 wbr
 |-  y 
20 19 17 0 wrex
 |-  E. z e. A y 
21 10 20 wi
 |-  ( y  E. z e. A y 
22 21 6 1 wral
 |-  A. y e. RR ( y  E. z e. A y 
23 16 22 wa
 |-  ( A. y e. A -. x  E. z e. A y 
24 23 5 1 wrex
 |-  E. x e. RR ( A. y e. A -. x  E. z e. A y 
25 13 24 wi
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y  E. x e. RR ( A. y e. A -. x  E. z e. A y