Metamath Proof Explorer

Theorem dib11N

Description: The isomorphism B for a lattice K is one-to-one in the region under co-atom W . (Contributed by NM, 24-Feb-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dib11.b ⊢ B = Base K
2 dib11.l ⊢ ≤ ˙ = ≤ K
3 dib11.h ⊢ H = LHyp ⁡ K
4 dib11.i ⊢ I = DIsoB ⁡ K ⁡ W
5 eqss ⊢ I ⁡ X = I ⁡ Y ↔ I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X
6 1 2 3 4 dibord ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ↔ X ≤ ˙ Y
7 1 2 3 4 dibord ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ B ∧ Y ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ Y ⊆ I ⁡ X ↔ Y ≤ ˙ X
8 7 3com23 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ Y ⊆ I ⁡ X ↔ Y ≤ ˙ X
9 6 8 anbi12d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X ↔ X ≤ ˙ Y ∧ Y ≤ ˙ X
10 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → K ∈ HL
11 10 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → K ∈ Lat
12 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → X ∈ B
13 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → Y ∈ B
14 1 2 latasymb ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
15 11 12 13 14 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
16 9 15 bitrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X ↔ X = Y
17 5 16 syl5bb ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X = I ⁡ Y ↔ X = Y