Theorem lautcl

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

	Ref	Expression
Hypotheses	laut1o.b	$$⊢B={\mathrm{Base}}_K$$
	laut1o.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
Assertion	lautcl	$$⊢\left(\left(K\in V\wedge F\in I\right)\wedge X\in B\right)\to F\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		laut1o.b	$$⊢B={\mathrm{Base}}_K$$
2		laut1o.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
3	1 2	laut1o	$$⊢\left(K\in V\wedge F\in I\right)\to F:B\underset{1-1\; onto}{⟶}B$$
4		f1of	$$⊢F:B\underset{1-1\; onto}{⟶}B\to F:B⟶B$$
5	3 4	syl	$$⊢\left(K\in V\wedge F\in I\right)\to F:B⟶B$$
6	5	ffvelcdmda	$$⊢\left(\left(K\in V\wedge F\in I\right)\wedge X\in B\right)\to F\left(X\right)\in B$$