Theorem lattr 18502

Description: A lattice ordering is transitive. (sstr 4004 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 18496	. 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
2		latref.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		latref.l	. . 3 ⊢ ≤ = (le‘𝐾)
4	2, 3	postr 18378	. 2 ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
5	1, 4	sylan 580	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106   class class class wbr 5148  ‘cfv 6563  Basecbs 17245  lecple 17305  Posetcpo 18365  Latclat 18489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-dm 5699  df-iota 6516  df-fv 6571  df-poset 18371  df-lat 18490

This theorem is referenced by:  lattrd  18504  latjlej1  18511  latjlej12  18513  latnlej2  18517  latmlem1  18527  latmlem12  18529  clatleglb  18576  lecmtN  39238  hlrelat2  39386  ps-2  39461  dalem3  39647  dalem17  39663  dalem21  39677  dalem25  39681  linepsubN  39735  pmapsub  39751  cdlemblem  39776  pmapjoin  39835  lhpmcvr4N  40009  4atexlemnclw  40053  cdlemd3  40183  cdleme3g  40217  cdleme3h  40218  cdleme7d  40229  cdleme21c  40310  cdleme32b  40425  cdleme35fnpq  40432  cdleme35f  40437  cdleme48bw  40485  cdlemf1  40544  cdlemg2fv2  40583  cdlemg7fvbwN  40590  cdlemg4  40600  cdlemg6c  40603  cdlemg27a  40675  cdlemg33b0  40684  cdlemg33a  40689  cdlemk3  40816  dia2dimlem1  41047  dihord6b  41243  dihord5apre  41245  dihglbcpreN  41283