Theorem lautcnvclN

Description: Reverse closure of a lattice automorphism. (Contributed by NM, 25-May-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	laut1o.b	$$⊢B={\mathrm{Base}}_K$$
	laut1o.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
Assertion	lautcnvclN	$$⊢\left(\left(K\in V\wedge F\in I\right)\wedge X\in B\right)\to F^{-1}\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		f1ocnvdm	$$⊢\left(F:B\underset{1-1\; onto}{⟶}B\wedge X\in B\right)\to F^{-1}\left(X\right)\in B$$
5	3 4	sylan	$$⊢\left(\left(K\in V\wedge F\in I\right)\wedge X\in B\right)\to F^{-1}\left(X\right)\in B$$