Theorem lattr 18489

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   class class class wbr 5143  ‘cfv 6561  Basecbs 17247  lecple 17304  Posetcpo 18353  Latclat 18476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-dm 5695  df-iota 6514  df-fv 6569  df-poset 18359  df-lat 18477

This theorem is referenced by:  lattrd  18491  latjlej1  18498  latjlej12  18500  latnlej2  18504  latmlem1  18514  latmlem12  18516  clatleglb  18563  lecmtN  39257  hlrelat2  39405  ps-2  39480  dalem3  39666  dalem17  39682  dalem21  39696  dalem25  39700  linepsubN  39754  pmapsub  39770  cdlemblem  39795  pmapjoin  39854  lhpmcvr4N  40028  4atexlemnclw  40072  cdlemd3  40202  cdleme3g  40236  cdleme3h  40237  cdleme7d  40248  cdleme21c  40329  cdleme32b  40444  cdleme35fnpq  40451  cdleme35f  40456  cdleme48bw  40504  cdlemf1  40563  cdlemg2fv2  40602  cdlemg7fvbwN  40609  cdlemg4  40619  cdlemg6c  40622  cdlemg27a  40694  cdlemg33b0  40703  cdlemg33a  40708  cdlemk3  40835  dia2dimlem1  41066  dihord6b  41262  dihord5apre  41264  dihglbcpreN  41302