Metamath Proof Explorer

Theorem lautcnv

Description: The converse of a lattice automorphism is a lattice automorphism. (Contributed by NM, 10-May-2013)

Ref Expression
Hypothesis lautcnv.i ⊢ I = LAut ⁡ K
Assertion lautcnv ⊢ K ∈ V ∧ F ∈ I → F -1 ∈ I

Proof

Step Hyp Ref Expression
1 lautcnv.i ⊢ I = LAut ⁡ K
2 eqid ⊢ Base K = Base K
3 2 1 laut1o ⊢ K ∈ V ∧ F ∈ I → F : Base K ⟶ 1-1 onto Base K
4 f1ocnv ⊢ F : Base K ⟶ 1-1 onto Base K → F -1 : Base K ⟶ 1-1 onto Base K
5 3 4 syl ⊢ K ∈ V ∧ F ∈ I → F -1 : Base K ⟶ 1-1 onto Base K
6 eqid ⊢ ≤ K = ≤ K
7 2 6 1 lautcnvle ⊢ K ∈ V ∧ F ∈ I ∧ x ∈ Base K ∧ y ∈ Base K → x ≤ K y ↔ F -1 ⁡ x ≤ K F -1 ⁡ y
8 7 ralrimivva ⊢ K ∈ V ∧ F ∈ I → ∀ x ∈ Base K ∀ y ∈ Base K x ≤ K y ↔ F -1 ⁡ x ≤ K F -1 ⁡ y
9 2 6 1 islaut ⊢ K ∈ V → F -1 ∈ I ↔ F -1 : Base K ⟶ 1-1 onto Base K ∧ ∀ x ∈ Base K ∀ y ∈ Base K x ≤ K y ↔ F -1 ⁡ x ≤ K F -1 ⁡ y
10 9 adantr ⊢ K ∈ V ∧ F ∈ I → F -1 ∈ I ↔ F -1 : Base K ⟶ 1-1 onto Base K ∧ ∀ x ∈ Base K ∀ y ∈ Base K x ≤ K y ↔ F -1 ⁡ x ≤ K F -1 ⁡ y
11 5 8 10 mpbir2and ⊢ K ∈ V ∧ F ∈ I → F -1 ∈ I