| 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 ) ) ) |