Metamath Proof Explorer


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 ) )