Theorem latasymd 18348

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

Hypotheses

Ref	Expression
latasymd.b	⊢ 𝐵 = (Base‘𝐾)
latasymd.l	⊢ ≤ = (le‘𝐾)
latasymd.3	⊢ (𝜑 → 𝐾 ∈ Lat)
latasymd.4	⊢ (𝜑 → 𝑋 ∈ 𝐵)
latasymd.5	⊢ (𝜑 → 𝑌 ∈ 𝐵)
latasymd.6	⊢ (𝜑 → 𝑋 ≤ 𝑌)
latasymd.7	⊢ (𝜑 → 𝑌 ≤ 𝑋)

Assertion

Ref	Expression
latasymd	⊢ (𝜑 → 𝑋 = 𝑌)

Proof of Theorem latasymd

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   class class class wbr 5110  ‘cfv 6501  Basecbs 17094  lecple 17154  Latclat 18334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5268

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-dm 5648  df-iota 6453  df-fv 6509  df-proset 18198  df-poset 18216  df-lat 18335

This theorem is referenced by:  latjidm  18365  latmidm  18377  latjass  18386  oldmm1  37752  olj01  37760  olm01  37771  cvlcvr1  37874  llnmlplnN  38075  2llnjaN  38102  2lplnja  38155  cdlema1N  38327  hlmod1i  38392  lautj  38629  lautm  38630  cdleme19a  38839  cdleme28b  38907  trljco  39276  dochvalr  39893