Metamath Proof Explorer


Theorem sup3

Description: A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004)

Ref Expression
Assertion sup3
|- ( ( 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 ssel
 |-  ( A C_ RR -> ( y e. A -> y e. RR ) )
2 leloe
 |-  ( ( y e. RR /\ x e. RR ) -> ( y <_ x <-> ( y < x \/ y = x ) ) )
3 2 expcom
 |-  ( x e. RR -> ( y e. RR -> ( y <_ x <-> ( y < x \/ y = x ) ) ) )
4 1 3 syl9
 |-  ( A C_ RR -> ( x e. RR -> ( y e. A -> ( y <_ x <-> ( y < x \/ y = x ) ) ) ) )
5 4 imp31
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( y <_ x <-> ( y < x \/ y = x ) ) )
6 5 ralbidva
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A y <_ x <-> A. y e. A ( y < x \/ y = x ) ) )
7 6 rexbidva
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A y <_ x <-> E. x e. RR A. y e. A ( y < x \/ y = x ) ) )
8 7 anbi2d
 |-  ( A C_ RR -> ( ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) )
9 8 pm5.32i
 |-  ( ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) )
10 3anass
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) )
11 3anass
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) )
12 9 10 11 3bitr4i
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) )
13 sup2
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
14 12 13 sylbi
 |-  ( ( 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 ) ) )