Metamath Proof Explorer


Theorem lautcl

Description: A lattice automorphism value belongs to the base set. (Contributed by NM, 20-May-2012)

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

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 f1of
 |-  ( F : B -1-1-onto-> B -> F : B --> B )
5 3 4 syl
 |-  ( ( K e. V /\ F e. I ) -> F : B --> B )
6 5 ffvelrnda
 |-  ( ( ( K e. V /\ F e. I ) /\ X e. B ) -> ( F ` X ) e. B )