Step |
Hyp |
Ref |
Expression |
1 |
|
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 ) ) ) |
2 |
|
ssel2 |
|- ( ( A C_ ZZ /\ x e. A ) -> x e. ZZ ) |
3 |
2
|
zred |
|- ( ( A C_ ZZ /\ x e. A ) -> x e. RR ) |
4 |
|
ltso |
|- < Or RR |
5 |
4
|
a1i |
|- ( T. -> < Or RR ) |
6 |
5
|
eqsup |
|- ( T. -> ( ( x e. RR /\ A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x ) ) |
7 |
6
|
mptru |
|- ( ( x e. RR /\ A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x ) |
8 |
7
|
3expib |
|- ( x e. RR -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x ) ) |
9 |
3 8
|
syl |
|- ( ( A C_ ZZ /\ x e. A ) -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x ) ) |
10 |
|
simpr |
|- ( ( A C_ ZZ /\ x e. A ) -> x e. A ) |
11 |
|
eleq1 |
|- ( sup ( A , RR , < ) = x -> ( sup ( A , RR , < ) e. A <-> x e. A ) ) |
12 |
10 11
|
syl5ibrcom |
|- ( ( A C_ ZZ /\ x e. A ) -> ( sup ( A , RR , < ) = x -> sup ( A , RR , < ) e. A ) ) |
13 |
9 12
|
syld |
|- ( ( A C_ ZZ /\ x e. A ) -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) e. A ) ) |
14 |
13
|
rexlimdva |
|- ( A C_ ZZ -> ( E. x e. A ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) e. A ) ) |
15 |
14
|
3ad2ant1 |
|- ( ( 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 ) ) -> sup ( A , RR , < ) e. A ) ) |
16 |
1 15
|
mpd |
|- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) -> sup ( A , RR , < ) e. A ) |