This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idlaut

Description: The identity function is a lattice automorphism. (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses idlaut.b 
|- B = ( Base ` K )
idlaut.i 
|- I = ( LAut ` K )
Assertion idlaut 
|- ( K e. A -> ( _I |` B ) e. I )

Proof

Step Hyp Ref Expression
1 idlaut.b 
 |-  B = ( Base ` K )
2 idlaut.i 
 |-  I = ( LAut ` K )
3 f1oi 
 |-  ( _I |` B ) : B -1-1-onto-> B
4 3 a1i 
 |-  ( K e. A -> ( _I |` B ) : B -1-1-onto-> B )
5 fvresi 
 |-  ( x e. B -> ( ( _I |` B ) ` x ) = x )
6 fvresi 
 |-  ( y e. B -> ( ( _I |` B ) ` y ) = y )
7 5 6 breqan12d 
 |-  ( ( x e. B /\ y e. B ) -> ( ( ( _I |` B ) ` x ) ( le ` K ) ( ( _I |` B ) ` y ) <-> x ( le ` K ) y ) )
8 7 bicomd 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( le ` K ) y <-> ( ( _I |` B ) ` x ) ( le ` K ) ( ( _I |` B ) ` y ) ) )
9 8 rgen2 
 |-  A. x e. B A. y e. B ( x ( le ` K ) y <-> ( ( _I |` B ) ` x ) ( le ` K ) ( ( _I |` B ) ` y ) )
10 9 a1i 
 |-  ( K e. A -> A. x e. B A. y e. B ( x ( le ` K ) y <-> ( ( _I |` B ) ` x ) ( le ` K ) ( ( _I |` B ) ` y ) ) )
11 eqid 
 |-  ( le ` K ) = ( le ` K )
12 1 11 2 islaut 
 |-  ( K e. A -> ( ( _I |` B ) e. I <-> ( ( _I |` B ) : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> ( ( _I |` B ) ` x ) ( le ` K ) ( ( _I |` B ) ` y ) ) ) ) )
13 4 10 12 mpbir2and 
 |-  ( K e. A -> ( _I |` B ) e. I )