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

Metamath Proof Explorer

Theorem axsup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion axsup 
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )

Proof

Step Hyp Ref Expression
1 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
2 1 3expia 
 |-  ( ( 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
3 ssel2 
 |-  ( ( A C_ RR /\ y e. A ) -> y e. RR )
4 ltxrlt 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y < x <-> y
5 3 4 sylan 
 |-  ( ( ( A C_ RR /\ y e. A ) /\ x e. RR ) -> ( y < x <-> y
6 5 an32s 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( y < x <-> y
7 6 ralbidva 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A y < x <-> A. y e. A y
8 7 rexbidva 
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A y < x <-> E. x e. RR A. y e. A y
9 8 adantr 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR A. y e. A y < x <-> E. x e. RR A. y e. A y
10 ltxrlt 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x < y <-> x
11 10 ancoms 
 |-  ( ( y e. RR /\ x e. RR ) -> ( x < y <-> x
12 3 11 sylan 
 |-  ( ( ( A C_ RR /\ y e. A ) /\ x e. RR ) -> ( x < y <-> x
13 12 an32s 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( x < y <-> x
14 13 notbid 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( -. x < y <-> -. x
15 14 ralbidva 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A -. x < y <-> A. y e. A -. x
16 4 ancoms 
 |-  ( ( x e. RR /\ y e. RR ) -> ( y < x <-> y
17 16 adantll 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. RR ) -> ( y < x <-> y
18 ssel2 
 |-  ( ( A C_ RR /\ z e. A ) -> z e. RR )
19 ltxrlt 
 |-  ( ( y e. RR /\ z e. RR ) -> ( y < z <-> y
20 19 ancoms 
 |-  ( ( z e. RR /\ y e. RR ) -> ( y < z <-> y
21 18 20 sylan 
 |-  ( ( ( A C_ RR /\ z e. A ) /\ y e. RR ) -> ( y < z <-> y
22 21 an32s 
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( y < z <-> y
23 22 rexbidva 
 |-  ( ( A C_ RR /\ y e. RR ) -> ( E. z e. A y < z <-> E. z e. A y
24 23 adantlr 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. RR ) -> ( E. z e. A y < z <-> E. z e. A y
25 17 24 imbi12d 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. RR ) -> ( ( y < x -> E. z e. A y < z ) <-> ( y  E. z e. A y
26 25 ralbidva 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. RR ( y < x -> E. z e. A y < z ) <-> A. y e. RR ( y  E. z e. A y
27 15 26 anbi12d 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) <-> ( A. y e. A -. x  E. z e. A y
28 27 rexbidva 
 |-  ( A C_ RR -> ( E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) <-> E. x e. RR ( A. y e. A -. x  E. z e. A y
29 28 adantr 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) <-> E. x e. RR ( A. y e. A -. x  E. z e. A y
30 2 9 29 3imtr4d 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR A. y e. A y < x -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) )
31 30 3impia 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )