Step |
Hyp |
Ref |
Expression |
1 |
|
ismntd.1 |
|- A = ( Base ` V ) |
2 |
|
ismntd.2 |
|- B = ( Base ` W ) |
3 |
|
ismntd.3 |
|- .<_ = ( le ` V ) |
4 |
|
ismntd.4 |
|- .c_ = ( le ` W ) |
5 |
|
ismntd.5 |
|- ( ph -> V e. C ) |
6 |
|
ismntd.6 |
|- ( ph -> W e. D ) |
7 |
|
ismntd.7 |
|- ( ph -> F e. ( V Monot W ) ) |
8 |
|
ismntd.8 |
|- ( ph -> X e. A ) |
9 |
|
ismntd.9 |
|- ( ph -> Y e. A ) |
10 |
|
ismntd.10 |
|- ( ph -> X .<_ Y ) |
11 |
1 2 3 4
|
ismnt |
|- ( ( V e. C /\ W e. D ) -> ( F e. ( V Monot W ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) ) |
12 |
11
|
biimp3a |
|- ( ( V e. C /\ W e. D /\ F e. ( V Monot W ) ) -> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) |
13 |
12
|
simprd |
|- ( ( V e. C /\ W e. D /\ F e. ( V Monot W ) ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) |
14 |
5 6 7 13
|
syl3anc |
|- ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) |
15 |
|
breq1 |
|- ( x = X -> ( x .<_ y <-> X .<_ y ) ) |
16 |
|
fveq2 |
|- ( x = X -> ( F ` x ) = ( F ` X ) ) |
17 |
16
|
breq1d |
|- ( x = X -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` X ) .c_ ( F ` y ) ) ) |
18 |
15 17
|
imbi12d |
|- ( x = X -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( X .<_ y -> ( F ` X ) .c_ ( F ` y ) ) ) ) |
19 |
|
breq2 |
|- ( y = Y -> ( X .<_ y <-> X .<_ Y ) ) |
20 |
|
fveq2 |
|- ( y = Y -> ( F ` y ) = ( F ` Y ) ) |
21 |
20
|
breq2d |
|- ( y = Y -> ( ( F ` X ) .c_ ( F ` y ) <-> ( F ` X ) .c_ ( F ` Y ) ) ) |
22 |
19 21
|
imbi12d |
|- ( y = Y -> ( ( X .<_ y -> ( F ` X ) .c_ ( F ` y ) ) <-> ( X .<_ Y -> ( F ` X ) .c_ ( F ` Y ) ) ) ) |
23 |
|
eqidd |
|- ( ( ph /\ x = X ) -> A = A ) |
24 |
18 22 8 23 9
|
rspc2vd |
|- ( ph -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) -> ( X .<_ Y -> ( F ` X ) .c_ ( F ` Y ) ) ) ) |
25 |
14 10 24
|
mp2d |
|- ( ph -> ( F ` X ) .c_ ( F ` Y ) ) |