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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
latasymd.l ⊢ ≤ = ( le ‘ 𝐾 )
latasymd.3 ⊢ ( 𝜑 → 𝐾 ∈ Lat )
latasymd.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
latasymd.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
latasymd.6 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
latasymd.7 ⊢ ( 𝜑 → 𝑌 ≤ 𝑋 )
Assertion latasymd ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 latasymd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 latasymd.l ⊢ ≤ = ( le ‘ 𝐾 )
3 latasymd.3 ⊢ ( 𝜑 → 𝐾 ∈ Lat )
4 latasymd.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 latasymd.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 latasymd.6 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
7 latasymd.7 ⊢ ( 𝜑 → 𝑌 ≤ 𝑋 )
8 1 2 latasymb ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )
9 3 4 5 8 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )
10 6 7 9 mpbi2and ⊢ ( 𝜑 → 𝑋 = 𝑌 )