Theorem laut11

Description: One-to-one property of a lattice automorphism. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	laut1o.b	|- B = ( Base ` K )
	laut1o.i	|- I = ( LAut ` K )
Assertion	laut11	|- ( ( ( K e. V /\ F e. I ) /\ ( X e. B /\ Y e. B ) ) -> ( ( F ` X ) = ( F ` Y ) <-> X = Y ) )

Proof

Step	Hyp	Ref	Expression
1		laut1o.b	|- B = ( Base ` K )
2		laut1o.i	|- I = ( LAut ` K )
3	1 2	laut1o	|- ( ( K e. V /\ F e. I ) -> F : B -1-1-onto-> B )
4		f1of1	|- ( F : B -1-1-onto-> B -> F : B -1-1-> B )
5	3 4	syl	|- ( ( K e. V /\ F e. I ) -> F : B -1-1-> B )
6		f1fveq	|- ( ( F : B -1-1-> B /\ ( X e. B /\ Y e. B ) ) -> ( ( F ` X ) = ( F ` Y ) <-> X = Y ) )
7	5 6	sylan	|- ( ( ( K e. V /\ F e. I ) /\ ( X e. B /\ Y e. B ) ) -> ( ( F ` X ) = ( F ` Y ) <-> X = Y ) )