Theorem laut1o

Description: A lattice automorphism is one-to-one and onto. (Contributed by NM, 19-May-2012)

	Ref	Expression
Hypotheses	laut1o.b	|- B = ( Base ` K )
	laut1o.i	|- I = ( LAut ` K )
Assertion	laut1o	|- ( ( K e. A /\ F e. I ) -> F : B -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		laut1o.b	|- B = ( Base ` K )
2		laut1o.i	|- I = ( LAut ` K )
3		eqid	|- ( le ` K ) = ( le ` K )
4	1 3 2	islaut	|- ( K e. A -> ( F e. I <-> ( F : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> ( F ` x ) ( le ` K ) ( F ` y ) ) ) ) )
5	4	simprbda	|- ( ( K e. A /\ F e. I ) -> F : B -1-1-onto-> B )