This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Base K
laut1o.i ⊢ I = LAut ⁡ K
Assertion lautcnvclN ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B → F -1 ⁡ X ∈ B

Proof

Step Hyp Ref Expression
1 laut1o.b ⊢ B = Base K
2 laut1o.i ⊢ I = LAut ⁡ K
3 1 2 laut1o ⊢ K ∈ V ∧ F ∈ I → F : B ⟶ 1-1 onto B
4 f1ocnvdm ⊢ F : B ⟶ 1-1 onto B ∧ X ∈ B → F -1 ⁡ X ∈ B
5 3 4 sylan ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B → F -1 ⁡ X ∈ B