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

Metamath Proof Explorer

Theorem latasymd

Description: Deduce equality from lattice ordering. ( eqssd analog.) (Contributed by NM, 18-Nov-2011)

Ref Expression
Hypotheses latasymd.b ⊢ B = Base K
latasymd.l ⊢ ≤ ˙ = ≤ K
latasymd.3 ⊢ φ → K ∈ Lat
latasymd.4 ⊢ φ → X ∈ B
latasymd.5 ⊢ φ → Y ∈ B
latasymd.6 ⊢ φ → X ≤ ˙ Y
latasymd.7 ⊢ φ → Y ≤ ˙ X
Assertion latasymd ⊢ φ → X = Y

Proof

Step Hyp Ref Expression
1 latasymd.b ⊢ B = Base K
2 latasymd.l ⊢ ≤ ˙ = ≤ K
3 latasymd.3 ⊢ φ → K ∈ Lat
4 latasymd.4 ⊢ φ → X ∈ B
5 latasymd.5 ⊢ φ → Y ∈ B
6 latasymd.6 ⊢ φ → X ≤ ˙ Y
7 latasymd.7 ⊢ φ → Y ≤ ˙ X
8 1 2 latasymb ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
9 3 4 5 8 syl3anc ⊢ φ → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
10 6 7 9 mpbi2and ⊢ φ → X = Y