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	⊢ ( 𝜑 → 𝑋 = 𝑌 )