Theorem lattr 18598

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6531  Basecbs 17367  lecple 17415  Posetcpo 18461  Latclat 18585

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-dm 5661  df-iota 6487  df-fv 6539  df-poset 18467  df-lat 18586

This theorem is used by:  lattrd  18600  latjlej1  18607  latjlej12  18609  latnlej2  18613  latmlem1  18623  latmlem12  18625  clatleglb  18672  lecmtN  40281  hlrelat2  40428  ps-2  40503  dalem3  40689  dalem17  40705  dalem21  40719  dalem25  40723  linepsubN  40777  pmapsub  40793  cdlemblem  40818  pmapjoin  40877  lhpmcvr4N  41051  4atexlemnclw  41095  cdlemd3  41225  cdleme3g  41259  cdleme3h  41260  cdleme7d  41271  cdleme21c  41352  cdleme32b  41467  cdleme35fnpq  41474  cdleme35f  41479  cdleme48bw  41527  cdlemf1  41586  cdlemg2fv2  41625  cdlemg7fvbwN  41632  cdlemg4  41642  cdlemg6c  41645  cdlemg27a  41717  cdlemg33b0  41726  cdlemg33a  41731  cdlemk3  41858  dia2dimlem1  42089  dihord6b  42285  dihord5apre  42287  dihglbcpreN  42325