Metamath Proof Explorer

Theorem lautset

Description: The set of lattice automorphisms. (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses lautset.b 
|- B = ( Base ` K )
lautset.l 
|- .<_ = ( le ` K )
lautset.i 
|- I = ( LAut ` K )
Assertion lautset 
|- ( K e. A -> I = { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } )

Proof

Step Hyp Ref Expression
1 lautset.b 
 |-  B = ( Base ` K )
2 lautset.l 
 |-  .<_ = ( le ` K )
3 lautset.i 
 |-  I = ( LAut ` K )
4 elex 
 |-  ( K e. A -> K e. _V )
5 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
6 5 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
7 6 f1oeq2d 
 |-  ( k = K -> ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) <-> f : B -1-1-onto-> ( Base ` k ) ) )
8 f1oeq3 
 |-  ( ( Base ` k ) = B -> ( f : B -1-1-onto-> ( Base ` k ) <-> f : B -1-1-onto-> B ) )
9 6 8 syl 
 |-  ( k = K -> ( f : B -1-1-onto-> ( Base ` k ) <-> f : B -1-1-onto-> B ) )
10 7 9 bitrd 
 |-  ( k = K -> ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) <-> f : B -1-1-onto-> B ) )
11 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
12 11 2 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
13 12 breqd 
 |-  ( k = K -> ( x ( le ` k ) y <-> x .<_ y ) )
14 12 breqd 
 |-  ( k = K -> ( ( f ` x ) ( le ` k ) ( f ` y ) <-> ( f ` x ) .<_ ( f ` y ) ) )
15 13 14 bibi12d 
 |-  ( k = K -> ( ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) <-> ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) )
16 6 15 raleqbidv 
 |-  ( k = K -> ( A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) <-> A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) )
17 6 16 raleqbidv 
 |-  ( k = K -> ( A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) <-> A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) )
18 10 17 anbi12d 
 |-  ( k = K -> ( ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) <-> ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) ) )
19 18 abbidv 
 |-  ( k = K -> { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) } = { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } )
20 df-laut 
 |-  LAut = ( k e. _V |-> { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) } )
21 1 fvexi 
 |-  B e. _V
22 21 21 mapval 
 |-  ( B ^m B ) = { f | f : B --> B }
23 ovex 
 |-  ( B ^m B ) e. _V
24 22 23 eqeltrri 
 |-  { f | f : B --> B } e. _V
25 f1of 
 |-  ( f : B -1-1-onto-> B -> f : B --> B )
26 25 ss2abi 
 |-  { f | f : B -1-1-onto-> B } C_ { f | f : B --> B }
27 24 26 ssexi 
 |-  { f | f : B -1-1-onto-> B } e. _V
28 simpl 
 |-  ( ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) -> f : B -1-1-onto-> B )
29 28 ss2abi 
 |-  { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } C_ { f | f : B -1-1-onto-> B }
30 27 29 ssexi 
 |-  { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } e. _V
31 19 20 30 fvmpt 
 |-  ( K e. _V -> ( LAut ` K ) = { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } )
32 3 31 syl5eq 
 |-  ( K e. _V -> I = { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } )
33 4 32 syl 
 |-  ( K e. A -> I = { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } )