This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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