Step |
Hyp |
Ref |
Expression |
1 |
|
lautco.i |
|- I = ( LAut ` K ) |
2 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
3 |
2 1
|
laut1o |
|- ( ( K e. V /\ F e. I ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
4 |
3
|
3adant3 |
|- ( ( K e. V /\ F e. I /\ G e. I ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
5 |
2 1
|
laut1o |
|- ( ( K e. V /\ G e. I ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
6 |
5
|
3adant2 |
|- ( ( K e. V /\ F e. I /\ G e. I ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
7 |
|
f1oco |
|- ( ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ G : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) -> ( F o. G ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
8 |
4 6 7
|
syl2anc |
|- ( ( K e. V /\ F e. I /\ G e. I ) -> ( F o. G ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
9 |
|
simpl1 |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> K e. V ) |
10 |
|
simpl2 |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> F e. I ) |
11 |
|
simpl3 |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> G e. I ) |
12 |
|
simprl |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> x e. ( Base ` K ) ) |
13 |
2 1
|
lautcl |
|- ( ( ( K e. V /\ G e. I ) /\ x e. ( Base ` K ) ) -> ( G ` x ) e. ( Base ` K ) ) |
14 |
9 11 12 13
|
syl21anc |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( G ` x ) e. ( Base ` K ) ) |
15 |
|
simprr |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> y e. ( Base ` K ) ) |
16 |
2 1
|
lautcl |
|- ( ( ( K e. V /\ G e. I ) /\ y e. ( Base ` K ) ) -> ( G ` y ) e. ( Base ` K ) ) |
17 |
9 11 15 16
|
syl21anc |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( G ` y ) e. ( Base ` K ) ) |
18 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
19 |
2 18 1
|
lautle |
|- ( ( ( K e. V /\ F e. I ) /\ ( ( G ` x ) e. ( Base ` K ) /\ ( G ` y ) e. ( Base ` K ) ) ) -> ( ( G ` x ) ( le ` K ) ( G ` y ) <-> ( F ` ( G ` x ) ) ( le ` K ) ( F ` ( G ` y ) ) ) ) |
20 |
9 10 14 17 19
|
syl22anc |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( ( G ` x ) ( le ` K ) ( G ` y ) <-> ( F ` ( G ` x ) ) ( le ` K ) ( F ` ( G ` y ) ) ) ) |
21 |
2 18 1
|
lautle |
|- ( ( ( K e. V /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( le ` K ) y <-> ( G ` x ) ( le ` K ) ( G ` y ) ) ) |
22 |
21
|
3adantl2 |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( le ` K ) y <-> ( G ` x ) ( le ` K ) ( G ` y ) ) ) |
23 |
|
f1of |
|- ( G : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> G : ( Base ` K ) --> ( Base ` K ) ) |
24 |
6 23
|
syl |
|- ( ( K e. V /\ F e. I /\ G e. I ) -> G : ( Base ` K ) --> ( Base ` K ) ) |
25 |
|
simpl |
|- ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> x e. ( Base ` K ) ) |
26 |
|
fvco3 |
|- ( ( G : ( Base ` K ) --> ( Base ` K ) /\ x e. ( Base ` K ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) ) |
27 |
24 25 26
|
syl2an |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) ) |
28 |
|
simpr |
|- ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> y e. ( Base ` K ) ) |
29 |
|
fvco3 |
|- ( ( G : ( Base ` K ) --> ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) ) |
30 |
24 28 29
|
syl2an |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) ) |
31 |
27 30
|
breq12d |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( ( ( F o. G ) ` x ) ( le ` K ) ( ( F o. G ) ` y ) <-> ( F ` ( G ` x ) ) ( le ` K ) ( F ` ( G ` y ) ) ) ) |
32 |
20 22 31
|
3bitr4d |
|- ( ( ( K e. V /\ F e. I /\ G e. I ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( le ` K ) y <-> ( ( F o. G ) ` x ) ( le ` K ) ( ( F o. G ) ` y ) ) ) |
33 |
32
|
ralrimivva |
|- ( ( K e. V /\ F e. I /\ G e. I ) -> A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( x ( le ` K ) y <-> ( ( F o. G ) ` x ) ( le ` K ) ( ( F o. G ) ` y ) ) ) |
34 |
2 18 1
|
islaut |
|- ( K e. V -> ( ( F o. G ) e. I <-> ( ( F o. G ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( x ( le ` K ) y <-> ( ( F o. G ) ` x ) ( le ` K ) ( ( F o. G ) ` y ) ) ) ) ) |
35 |
34
|
3ad2ant1 |
|- ( ( K e. V /\ F e. I /\ G e. I ) -> ( ( F o. G ) e. I <-> ( ( F o. G ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( x ( le ` K ) y <-> ( ( F o. G ) ` x ) ( le ` K ) ( ( F o. G ) ` y ) ) ) ) ) |
36 |
8 33 35
|
mpbir2and |
|- ( ( K e. V /\ F e. I /\ G e. I ) -> ( F o. G ) e. I ) |