Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> A C_ ZZ ) |
2 |
|
zssre |
|- ZZ C_ RR |
3 |
1 2
|
sstrdi |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> A C_ RR ) |
4 |
|
simp3 |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> B e. A ) |
5 |
3 4
|
sseldd |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> B e. RR ) |
6 |
4
|
ne0d |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> A =/= (/) ) |
7 |
|
simp2 |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> E. x e. ZZ A. y e. A y <_ x ) |
8 |
|
suprzcl2 |
|- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) -> sup ( A , RR , < ) e. A ) |
9 |
1 6 7 8
|
syl3anc |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> sup ( A , RR , < ) e. A ) |
10 |
3 9
|
sseldd |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> sup ( A , RR , < ) e. RR ) |
11 |
|
ltso |
|- < Or RR |
12 |
11
|
a1i |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> < Or RR ) |
13 |
|
zsupss |
|- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) |
14 |
1 6 7 13
|
syl3anc |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) |
15 |
|
ssrexv |
|- ( A C_ RR -> ( E. x e. A ( 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 < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) ) |
16 |
3 14 15
|
sylc |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) |
17 |
12 16
|
supub |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> ( B e. A -> -. sup ( A , RR , < ) < B ) ) |
18 |
4 17
|
mpd |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> -. sup ( A , RR , < ) < B ) |
19 |
5 10 18
|
nltled |
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> B <_ sup ( A , RR , < ) ) |