Metamath Proof Explorer

Theorem diaord

Description: The partial isomorphism A for a lattice K is order-preserving in the region under co-atom W . Part of Lemma M of Crawley p. 120 line 28. (Contributed by NM, 26-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 dia11.b ⊢ B = Base K
2 dia11.l ⊢ ≤ ˙ = ≤ K
3 dia11.h ⊢ H = LHyp ⁡ K
4 dia11.i ⊢ I = DIsoA ⁡ K ⁡ W
5 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
6 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
7 1 2 3 5 6 4 diaval ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X
8 7 3adant3 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X = f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X
9 1 2 3 5 6 4 diaval ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ Y = f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ Y
10 9 3adant2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ Y = f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ Y
11 8 10 sseq12d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ↔ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X ⊆ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ Y
12 ss2rab ⊢ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X ⊆ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ Y ↔ ∀ f ∈ LTrn ⁡ K ⁡ W trL ⁡ K ⁡ W ⁡ f ≤ ˙ X → trL ⁡ K ⁡ W ⁡ f ≤ ˙ Y
13 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
14 1 2 13 3 5 6 trlord ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → X ≤ ˙ Y ↔ ∀ f ∈ LTrn ⁡ K ⁡ W trL ⁡ K ⁡ W ⁡ f ≤ ˙ X → trL ⁡ K ⁡ W ⁡ f ≤ ˙ Y
15 12 14 bitr4id ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X ⊆ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ Y ↔ X ≤ ˙ Y
16 11 15 bitrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ↔ X ≤ ˙ Y