Step |
Hyp |
Ref |
Expression |
1 |
|
ssrab2 |
|- { x e. ZZ | x <_ A } C_ ZZ |
2 |
|
zssre |
|- ZZ C_ RR |
3 |
1 2
|
sstri |
|- { x e. ZZ | x <_ A } C_ RR |
4 |
3
|
a1i |
|- ( A e. RR -> { x e. ZZ | x <_ A } C_ RR ) |
5 |
|
breq1 |
|- ( x = ( |_ ` A ) -> ( x <_ A <-> ( |_ ` A ) <_ A ) ) |
6 |
|
flcl |
|- ( A e. RR -> ( |_ ` A ) e. ZZ ) |
7 |
|
flle |
|- ( A e. RR -> ( |_ ` A ) <_ A ) |
8 |
5 6 7
|
elrabd |
|- ( A e. RR -> ( |_ ` A ) e. { x e. ZZ | x <_ A } ) |
9 |
8
|
ne0d |
|- ( A e. RR -> { x e. ZZ | x <_ A } =/= (/) ) |
10 |
|
reflcl |
|- ( A e. RR -> ( |_ ` A ) e. RR ) |
11 |
|
breq1 |
|- ( x = z -> ( x <_ A <-> z <_ A ) ) |
12 |
11
|
elrab |
|- ( z e. { x e. ZZ | x <_ A } <-> ( z e. ZZ /\ z <_ A ) ) |
13 |
|
flge |
|- ( ( A e. RR /\ z e. ZZ ) -> ( z <_ A <-> z <_ ( |_ ` A ) ) ) |
14 |
13
|
biimpd |
|- ( ( A e. RR /\ z e. ZZ ) -> ( z <_ A -> z <_ ( |_ ` A ) ) ) |
15 |
14
|
expimpd |
|- ( A e. RR -> ( ( z e. ZZ /\ z <_ A ) -> z <_ ( |_ ` A ) ) ) |
16 |
12 15
|
syl5bi |
|- ( A e. RR -> ( z e. { x e. ZZ | x <_ A } -> z <_ ( |_ ` A ) ) ) |
17 |
16
|
ralrimiv |
|- ( A e. RR -> A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) ) |
18 |
|
brralrspcev |
|- ( ( ( |_ ` A ) e. RR /\ A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) ) -> E. y e. RR A. z e. { x e. ZZ | x <_ A } z <_ y ) |
19 |
10 17 18
|
syl2anc |
|- ( A e. RR -> E. y e. RR A. z e. { x e. ZZ | x <_ A } z <_ y ) |
20 |
4 9 19 8
|
suprubd |
|- ( A e. RR -> ( |_ ` A ) <_ sup ( { x e. ZZ | x <_ A } , RR , < ) ) |
21 |
|
suprleub |
|- ( ( ( { x e. ZZ | x <_ A } C_ RR /\ { x e. ZZ | x <_ A } =/= (/) /\ E. y e. RR A. z e. { x e. ZZ | x <_ A } z <_ y ) /\ ( |_ ` A ) e. RR ) -> ( sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) <-> A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) ) ) |
22 |
4 9 19 10 21
|
syl31anc |
|- ( A e. RR -> ( sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) <-> A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) ) ) |
23 |
17 22
|
mpbird |
|- ( A e. RR -> sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) ) |
24 |
4 9 19
|
suprcld |
|- ( A e. RR -> sup ( { x e. ZZ | x <_ A } , RR , < ) e. RR ) |
25 |
10 24
|
letri3d |
|- ( A e. RR -> ( ( |_ ` A ) = sup ( { x e. ZZ | x <_ A } , RR , < ) <-> ( ( |_ ` A ) <_ sup ( { x e. ZZ | x <_ A } , RR , < ) /\ sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) ) ) ) |
26 |
20 23 25
|
mpbir2and |
|- ( A e. RR -> ( |_ ` A ) = sup ( { x e. ZZ | x <_ A } , RR , < ) ) |