Step |
Hyp |
Ref |
Expression |
1 |
|
flle |
|- ( A e. RR -> ( |_ ` A ) <_ A ) |
2 |
|
flge |
|- ( ( A e. RR /\ y e. ZZ ) -> ( y <_ A <-> y <_ ( |_ ` A ) ) ) |
3 |
2
|
biimpd |
|- ( ( A e. RR /\ y e. ZZ ) -> ( y <_ A -> y <_ ( |_ ` A ) ) ) |
4 |
3
|
ralrimiva |
|- ( A e. RR -> A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) |
5 |
|
flcl |
|- ( A e. RR -> ( |_ ` A ) e. ZZ ) |
6 |
|
zmax |
|- ( A e. RR -> E! x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) |
7 |
|
breq1 |
|- ( x = ( |_ ` A ) -> ( x <_ A <-> ( |_ ` A ) <_ A ) ) |
8 |
|
breq2 |
|- ( x = ( |_ ` A ) -> ( y <_ x <-> y <_ ( |_ ` A ) ) ) |
9 |
8
|
imbi2d |
|- ( x = ( |_ ` A ) -> ( ( y <_ A -> y <_ x ) <-> ( y <_ A -> y <_ ( |_ ` A ) ) ) ) |
10 |
9
|
ralbidv |
|- ( x = ( |_ ` A ) -> ( A. y e. ZZ ( y <_ A -> y <_ x ) <-> A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) ) |
11 |
7 10
|
anbi12d |
|- ( x = ( |_ ` A ) -> ( ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) <-> ( ( |_ ` A ) <_ A /\ A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) ) ) |
12 |
11
|
riota2 |
|- ( ( ( |_ ` A ) e. ZZ /\ E! x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) -> ( ( ( |_ ` A ) <_ A /\ A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) = ( |_ ` A ) ) ) |
13 |
5 6 12
|
syl2anc |
|- ( A e. RR -> ( ( ( |_ ` A ) <_ A /\ A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) = ( |_ ` A ) ) ) |
14 |
1 4 13
|
mpbi2and |
|- ( A e. RR -> ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) = ( |_ ` A ) ) |
15 |
14
|
eqcomd |
|- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) ) |