Step |
Hyp |
Ref |
Expression |
1 |
|
lautset.b |
|- B = ( Base ` K ) |
2 |
|
lautset.l |
|- .<_ = ( le ` K ) |
3 |
|
lautset.i |
|- I = ( LAut ` K ) |
4 |
1 2 3
|
islaut |
|- ( K e. V -> ( F e. I <-> ( F : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) ) ) |
5 |
4
|
simplbda |
|- ( ( K e. V /\ F e. I ) -> A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) |
6 |
|
breq1 |
|- ( x = X -> ( x .<_ y <-> X .<_ y ) ) |
7 |
|
fveq2 |
|- ( x = X -> ( F ` x ) = ( F ` X ) ) |
8 |
7
|
breq1d |
|- ( x = X -> ( ( F ` x ) .<_ ( F ` y ) <-> ( F ` X ) .<_ ( F ` y ) ) ) |
9 |
6 8
|
bibi12d |
|- ( x = X -> ( ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) <-> ( X .<_ y <-> ( F ` X ) .<_ ( F ` y ) ) ) ) |
10 |
|
breq2 |
|- ( y = Y -> ( X .<_ y <-> X .<_ Y ) ) |
11 |
|
fveq2 |
|- ( y = Y -> ( F ` y ) = ( F ` Y ) ) |
12 |
11
|
breq2d |
|- ( y = Y -> ( ( F ` X ) .<_ ( F ` y ) <-> ( F ` X ) .<_ ( F ` Y ) ) ) |
13 |
10 12
|
bibi12d |
|- ( y = Y -> ( ( X .<_ y <-> ( F ` X ) .<_ ( F ` y ) ) <-> ( X .<_ Y <-> ( F ` X ) .<_ ( F ` Y ) ) ) ) |
14 |
9 13
|
rspc2v |
|- ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) -> ( X .<_ Y <-> ( F ` X ) .<_ ( F ` Y ) ) ) ) |
15 |
5 14
|
mpan9 |
|- ( ( ( K e. V /\ F e. I ) /\ ( X e. B /\ Y e. B ) ) -> ( X .<_ Y <-> ( F ` X ) .<_ ( F ` Y ) ) ) |