Metamath Proof Explorer

Theorem islaut

Description: The predictate "is a lattice automorphism." (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses lautset.b 
|- B = ( Base ` K )
lautset.l 
|- .<_ = ( le ` K )
lautset.i 
|- I = ( LAut ` K )
Assertion islaut 
|- ( K e. A -> ( F e. I <-> ( 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 1 2 3 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 ) ) ) } )
5 4 eleq2d 
 |-  ( K e. A -> ( F e. I <-> F e. { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } ) )
6 f1of 
 |-  ( F : B -1-1-onto-> B -> F : B --> B )
7 1 fvexi 
 |-  B e. _V
8 fex 
 |-  ( ( F : B --> B /\ B e. _V ) -> F e. _V )
9 6 7 8 sylancl 
 |-  ( F : B -1-1-onto-> B -> F e. _V )
10 9 adantr 
 |-  ( ( F : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) -> F e. _V )
11 f1oeq1 
 |-  ( f = F -> ( f : B -1-1-onto-> B <-> F : B -1-1-onto-> B ) )
12 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
13 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
14 12 13 breq12d 
 |-  ( f = F -> ( ( f ` x ) .<_ ( f ` y ) <-> ( F ` x ) .<_ ( F ` y ) ) )
15 14 bibi2d 
 |-  ( f = F -> ( ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) <-> ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) )
16 15 2ralbidv 
 |-  ( f = F -> ( A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) <-> A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) )
17 11 16 anbi12d 
 |-  ( f = F -> ( ( 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 /\ A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) ) )
18 10 17 elab3 
 |-  ( F e. { f | ( 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 /\ A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) )
19 5 18 bitrdi 
 |-  ( K e. A -> ( F e. I <-> ( F : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) ) )