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

Metamath Proof Explorer

Theorem lautle

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

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

Proof

Step Hyp Ref Expression
1 lautset.b ⊢ B = Base K
2 lautset.l ⊢ ≤ ˙ = ≤ K
3 lautset.i ⊢ I = LAut ⁡ K
4 1 2 3 islaut ⊢ K ∈ V → F ∈ I ↔ F : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ F ⁡ x ≤ ˙ F ⁡ y
5 4 simplbda ⊢ K ∈ V ∧ F ∈ I → ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ F ⁡ x ≤ ˙ F ⁡ y
6 breq1 ⊢ x = X → x ≤ ˙ y ↔ X ≤ ˙ y
7 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
8 7 breq1d ⊢ x = X → F ⁡ x ≤ ˙ F ⁡ y ↔ F ⁡ X ≤ ˙ F ⁡ y
9 6 8 bibi12d ⊢ x = X → x ≤ ˙ y ↔ F ⁡ x ≤ ˙ F ⁡ y ↔ X ≤ ˙ y ↔ F ⁡ X ≤ ˙ F ⁡ y
10 breq2 ⊢ y = Y → X ≤ ˙ y ↔ X ≤ ˙ Y
11 fveq2 ⊢ y = Y → F ⁡ y = F ⁡ Y
12 11 breq2d ⊢ y = Y → F ⁡ X ≤ ˙ F ⁡ y ↔ F ⁡ X ≤ ˙ F ⁡ Y
13 10 12 bibi12d ⊢ y = Y → X ≤ ˙ y ↔ F ⁡ X ≤ ˙ F ⁡ y ↔ X ≤ ˙ Y ↔ F ⁡ X ≤ ˙ F ⁡ Y
14 9 13 rspc2v ⊢ X ∈ B ∧ Y ∈ B → ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ F ⁡ x ≤ ˙ F ⁡ y → X ≤ ˙ Y ↔ F ⁡ X ≤ ˙ F ⁡ Y
15 5 14 mpan9 ⊢ K ∈ V ∧ F ∈ I ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F ⁡ X ≤ ˙ F ⁡ Y