Theorem lattrd 18173

Description: A lattice ordering is transitive. Deduction version of lattr 18171. (Contributed by NM, 3-Sep-2012.)

Hypotheses

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

Assertion

Ref	Expression
lattrd	⊢ (𝜑 → 𝑋 ≤ 𝑍)

Proof of Theorem lattrd

Step	Hyp	Ref	Expression
1		lattrd.5	. 2 ⊢ (𝜑 → 𝑋 ≤ 𝑌)
2		lattrd.6	. 2 ⊢ (𝜑 → 𝑌 ≤ 𝑍)
3		lattrd.1	. . 3 ⊢ (𝜑 → 𝐾 ∈ Lat)
4		lattrd.2	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
5		lattrd.3	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
6		lattrd.4	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
7		lattrd.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		lattrd.l	. . . 4 ⊢ ≤ = (le‘𝐾)
9	7, 8	lattr 18171	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
10	3, 4, 5, 6, 9	syl13anc 1371	. 2 ⊢ (𝜑 → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
11	1, 2, 10	mp2and 696	1 ⊢ (𝜑 → 𝑋 ≤ 𝑍)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107   class class class wbr 5075  ‘cfv 6437  Basecbs 16921  lecple 16978  Latclat 18158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-xp 5596  df-dm 5600  df-iota 6395  df-fv 6445  df-poset 18040  df-lat 18159

This theorem is referenced by:  latmlej11  18205  latjass  18210  lubun  18242  cvlcvr1  37360  exatleN  37425  2atjm  37466  2llnmat  37545  llnmlplnN  37560  2llnjaN  37587  2lplnja  37640  dalem5  37688  lncmp  37804  2lnat  37805  2llnma1b  37807  cdlema1N  37812  paddasslem5  37845  paddasslem12  37852  paddasslem13  37853  dalawlem3  37894  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem11  37902  dalawlem12  37903  pl42lem1N  38000  lhpexle2lem  38030  lhpexle3lem  38032  4atexlemtlw  38088  4atexlemc  38090  cdleme15  38299  cdleme17b  38308  cdleme22e  38365  cdleme22eALTN  38366  cdleme23a  38370  cdleme28a  38391  cdleme30a  38399  cdleme32e  38466  cdleme35b  38471  trlord  38590  cdlemg10  38662  cdlemg11b  38663  cdlemg17a  38682  cdlemg35  38734  tendococl  38793  tendopltp  38801  cdlemi1  38839  cdlemk11  38870  cdlemk5u  38882  cdlemk11u  38892  cdlemk52  38975  dialss  39067  diaglbN  39076  diaintclN  39079  dia2dimlem1  39085  cdlemm10N  39139  djajN  39158  dibglbN  39187  dibintclN  39188  diblss  39191  cdlemn10  39227  dihord1  39239  dihord2pre2  39247  dihopelvalcpre  39269  dihord5apre  39283  dihmeetlem1N  39311  dihglblem2N  39315  dihmeetlem2N  39320  dihglbcpreN  39321  dihmeetlem3N  39326