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 )