Metamath Proof Explorer

Theorem sup2

Description: A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
2 1 adantr 
 |-  ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> ( x + 1 ) e. RR )
3 2 a1i 
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> ( x + 1 ) e. RR ) )
4 ssel 
 |-  ( A C_ RR -> ( y e. A -> y e. RR ) )
5 ltp1 
 |-  ( x e. RR -> x < ( x + 1 ) )
6 1 ancli 
 |-  ( x e. RR -> ( x e. RR /\ ( x + 1 ) e. RR ) )
7 lttr 
 |-  ( ( y e. RR /\ x e. RR /\ ( x + 1 ) e. RR ) -> ( ( y < x /\ x < ( x + 1 ) ) -> y < ( x + 1 ) ) )
8 7 3expb 
 |-  ( ( y e. RR /\ ( x e. RR /\ ( x + 1 ) e. RR ) ) -> ( ( y < x /\ x < ( x + 1 ) ) -> y < ( x + 1 ) ) )
9 6 8 sylan2 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( y < x /\ x < ( x + 1 ) ) -> y < ( x + 1 ) ) )
10 5 9 sylan2i 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( y < x /\ x e. RR ) -> y < ( x + 1 ) ) )
11 10 exp4b 
 |-  ( y e. RR -> ( x e. RR -> ( y < x -> ( x e. RR -> y < ( x + 1 ) ) ) ) )
12 11 com34 
 |-  ( y e. RR -> ( x e. RR -> ( x e. RR -> ( y < x -> y < ( x + 1 ) ) ) ) )
13 12 pm2.43d 
 |-  ( y e. RR -> ( x e. RR -> ( y < x -> y < ( x + 1 ) ) ) )
14 13 imp 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y < x -> y < ( x + 1 ) ) )
15 breq1 
 |-  ( y = x -> ( y < ( x + 1 ) <-> x < ( x + 1 ) ) )
16 5 15 syl5ibrcom 
 |-  ( x e. RR -> ( y = x -> y < ( x + 1 ) ) )
17 16 adantl 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y = x -> y < ( x + 1 ) ) )
18 14 17 jaod 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) )
19 18 ex 
 |-  ( y e. RR -> ( x e. RR -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) )
20 4 19 syl6 
 |-  ( A C_ RR -> ( y e. A -> ( x e. RR -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) ) )
21 20 com23 
 |-  ( A C_ RR -> ( x e. RR -> ( y e. A -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) ) )
22 21 imp 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( y e. A -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) )
23 22 a2d 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( ( y e. A -> ( y < x \/ y = x ) ) -> ( y e. A -> y < ( x + 1 ) ) ) )
24 23 ralimdv2 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A ( y < x \/ y = x ) -> A. y e. A y < ( x + 1 ) ) )
25 24 expimpd 
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> A. y e. A y < ( x + 1 ) ) )
26 3 25 jcad 
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> ( ( x + 1 ) e. RR /\ A. y e. A y < ( x + 1 ) ) ) )
27 ovex 
 |-  ( x + 1 ) e. _V
28 eleq1 
 |-  ( z = ( x + 1 ) -> ( z e. RR <-> ( x + 1 ) e. RR ) )
29 breq2 
 |-  ( z = ( x + 1 ) -> ( y < z <-> y < ( x + 1 ) ) )
30 29 ralbidv 
 |-  ( z = ( x + 1 ) -> ( A. y e. A y < z <-> A. y e. A y < ( x + 1 ) ) )
31 28 30 anbi12d 
 |-  ( z = ( x + 1 ) -> ( ( z e. RR /\ A. y e. A y < z ) <-> ( ( x + 1 ) e. RR /\ A. y e. A y < ( x + 1 ) ) ) )
32 27 31 spcev 
 |-  ( ( ( x + 1 ) e. RR /\ A. y e. A y < ( x + 1 ) ) -> E. z ( z e. RR /\ A. y e. A y < z ) )
33 26 32 syl6 
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> E. z ( z e. RR /\ A. y e. A y < z ) ) )
34 33 exlimdv 
 |-  ( A C_ RR -> ( E. x ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> E. z ( z e. RR /\ A. y e. A y < z ) ) )
35 eleq1 
 |-  ( z = x -> ( z e. RR <-> x e. RR ) )
36 breq2 
 |-  ( z = x -> ( y < z <-> y < x ) )
37 36 ralbidv 
 |-  ( z = x -> ( A. y e. A y < z <-> A. y e. A y < x ) )
38 35 37 anbi12d 
 |-  ( z = x -> ( ( z e. RR /\ A. y e. A y < z ) <-> ( x e. RR /\ A. y e. A y < x ) ) )
39 38 cbvexvw 
 |-  ( E. z ( z e. RR /\ A. y e. A y < z ) <-> E. x ( x e. RR /\ A. y e. A y < x ) )
40 34 39 syl6ib 
 |-  ( A C_ RR -> ( E. x ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> E. x ( x e. RR /\ A. y e. A y < x ) ) )
41 df-rex 
 |-  ( E. x e. RR A. y e. A ( y < x \/ y = x ) <-> E. x ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) )
42 df-rex 
 |-  ( E. x e. RR A. y e. A y < x <-> E. x ( x e. RR /\ A. y e. A y < x ) )
43 40 41 42 3imtr4g 
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A ( y < x \/ y = x ) -> E. x e. RR A. y e. A y < x ) )
44 43 adantr 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR A. y e. A ( y < x \/ y = x ) -> E. x e. RR A. y e. A y < x ) )
45 44 imdistani 
 |-  ( ( ( 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 ) )
46 df-3an 
 |-  ( ( 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 ) ) )
47 df-3an 
 |-  ( ( 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 ) )
48 45 46 47 3imtr4i 
 |-  ( ( 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 ) )
49 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 ) ) )
50 48 49 syl 
 |-  ( ( 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 ) ) )