Metamath Proof Explorer

Theorem dihord3

Description: The isomorphism H for a lattice K is order-preserving in the region under co-atom W . (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihord3.b ⊢ B = Base K
dihord3.l ⊢ ≤ ˙ = ≤ K
dihord3.h ⊢ H = LHyp ⁡ K
dihord3.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihord3 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ↔ X ≤ ˙ Y

Proof

Step Hyp Ref Expression
1 dihord3.b ⊢ B = Base K
2 dihord3.l ⊢ ≤ ˙ = ≤ K
3 dihord3.h ⊢ H = LHyp ⁡ K
4 dihord3.i ⊢ I = DIsoH ⁡ K ⁡ W
5 eqid ⊢ DIsoB ⁡ K ⁡ W = DIsoB ⁡ K ⁡ W
6 1 2 3 4 5 dihvalb ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = DIsoB ⁡ K ⁡ W ⁡ X
7 6 3adant3 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X = DIsoB ⁡ K ⁡ W ⁡ X
8 1 2 3 4 5 dihvalb ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ Y = DIsoB ⁡ K ⁡ W ⁡ Y
9 8 3adant2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ Y = DIsoB ⁡ K ⁡ W ⁡ Y
10 7 9 sseq12d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ↔ DIsoB ⁡ K ⁡ W ⁡ X ⊆ DIsoB ⁡ K ⁡ W ⁡ Y
11 1 2 3 5 dibord ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → DIsoB ⁡ K ⁡ W ⁡ X ⊆ DIsoB ⁡ K ⁡ W ⁡ Y ↔ X ≤ ˙ Y
12 10 11 bitrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ↔ X ≤ ˙ Y