Theorem lattr 18350

Description: A lattice ordering is transitive. (sstr 3943 analog.) (Contributed by NM, 17-Nov-2011.)

Hypotheses

Ref	Expression
latref.b	⊢ 𝐵 = (Base‘𝐾)
latref.l	⊢ ≤ = (le‘𝐾)

Assertion

Ref	Expression
lattr	⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))

Proof of Theorem lattr

Step	Hyp	Ref	Expression
1		latpos 18344	. 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
2		latref.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		latref.l	. . 3 ⊢ ≤ = (le‘𝐾)
4	2, 3	postr 18226	. 2 ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
5	1, 4	sylan 580	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   class class class wbr 5091  ‘cfv 6481  Basecbs 17120  lecple 17168  Posetcpo 18213  Latclat 18337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-xp 5622  df-dm 5626  df-iota 6437  df-fv 6489  df-poset 18219  df-lat 18338

This theorem is referenced by:  lattrd  18352  latjlej1  18359  latjlej12  18361  latnlej2  18365  latmlem1  18375  latmlem12  18377  clatleglb  18424  lecmtN  39301  hlrelat2  39448  ps-2  39523  dalem3  39709  dalem17  39725  dalem21  39739  dalem25  39743  linepsubN  39797  pmapsub  39813  cdlemblem  39838  pmapjoin  39897  lhpmcvr4N  40071  4atexlemnclw  40115  cdlemd3  40245  cdleme3g  40279  cdleme3h  40280  cdleme7d  40291  cdleme21c  40372  cdleme32b  40487  cdleme35fnpq  40494  cdleme35f  40499  cdleme48bw  40547  cdlemf1  40606  cdlemg2fv2  40645  cdlemg7fvbwN  40652  cdlemg4  40662  cdlemg6c  40665  cdlemg27a  40737  cdlemg33b0  40746  cdlemg33a  40751  cdlemk3  40878  dia2dimlem1  41109  dihord6b  41305  dihord5apre  41307  dihglbcpreN  41345