Metamath Proof Explorer

Theorem lautcnvle

Description: Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012)

Ref Expression
Hypotheses lautcnvle.b ⊢ B = Base K
lautcnvle.l ⊢ ≤ ˙ = ≤ K
lautcnvle.i ⊢ I = LAut ⁡ K
Assertion lautcnvle ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F -1 ⁡ X ≤ ˙ F -1 ⁡ Y

Proof

Step Hyp Ref Expression
1 lautcnvle.b ⊢ B = Base K
2 lautcnvle.l ⊢ ≤ ˙ = ≤ K
3 lautcnvle.i ⊢ I = LAut ⁡ K
4 simpl ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → K ∈ V ∧ F ∈ I
5 1 3 laut1o ⊢ K ∈ V ∧ F ∈ I → F : B ⟶ 1-1 onto B
6 5 adantr ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → F : B ⟶ 1-1 onto B
7 simprl ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → X ∈ B
8 f1ocnvdm ⊢ F : B ⟶ 1-1 onto B ∧ X ∈ B → F -1 ⁡ X ∈ B
9 6 7 8 syl2anc ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → F -1 ⁡ X ∈ B
10 simprr ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
11 f1ocnvdm ⊢ F : B ⟶ 1-1 onto B ∧ Y ∈ B → F -1 ⁡ Y ∈ B
12 6 10 11 syl2anc ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → F -1 ⁡ Y ∈ B
13 1 2 3 lautle ⊢ K ∈ V ∧ F ∈ I ∧ F -1 ⁡ X ∈ B ∧ F -1 ⁡ Y ∈ B → F -1 ⁡ X ≤ ˙ F -1 ⁡ Y ↔ F ⁡ F -1 ⁡ X ≤ ˙ F ⁡ F -1 ⁡ Y
14 4 9 12 13 syl12anc ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → F -1 ⁡ X ≤ ˙ F -1 ⁡ Y ↔ F ⁡ F -1 ⁡ X ≤ ˙ F ⁡ F -1 ⁡ Y
15 f1ocnvfv2 ⊢ F : B ⟶ 1-1 onto B ∧ X ∈ B → F ⁡ F -1 ⁡ X = X
16 6 7 15 syl2anc ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → F ⁡ F -1 ⁡ X = X
17 f1ocnvfv2 ⊢ F : B ⟶ 1-1 onto B ∧ Y ∈ B → F ⁡ F -1 ⁡ Y = Y
18 6 10 17 syl2anc ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → F ⁡ F -1 ⁡ Y = Y
19 16 18 breq12d ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → F ⁡ F -1 ⁡ X ≤ ˙ F ⁡ F -1 ⁡ Y ↔ X ≤ ˙ Y
20 14 19 bitr2d ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F -1 ⁡ X ≤ ˙ F -1 ⁡ Y