Theorem lattrd 18381

Description: A lattice ordering is transitive. Deduction version of lattr 18379. (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 18379	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
10	3, 4, 5, 6, 9	syl13anc 1375	. 2 ⊢ (𝜑 → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
11	1, 2, 10	mp2and 700	1 ⊢ (𝜑 → 𝑋 ≤ 𝑍)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6500  Basecbs 17148  lecple 17196  Latclat 18366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-dm 5642  df-iota 6456  df-fv 6508  df-poset 18248  df-lat 18367

This theorem is referenced by:  latmlej11  18413  latjass  18418  lubun  18450  cvlcvr1  39709  exatleN  39774  2atjm  39815  2llnmat  39894  llnmlplnN  39909  2llnjaN  39936  2lplnja  39989  dalem5  40037  lncmp  40153  2lnat  40154  2llnma1b  40156  cdlema1N  40161  paddasslem5  40194  paddasslem12  40201  paddasslem13  40202  dalawlem3  40243  dalawlem5  40245  dalawlem6  40246  dalawlem7  40247  dalawlem8  40248  dalawlem11  40251  dalawlem12  40252  pl42lem1N  40349  lhpexle2lem  40379  lhpexle3lem  40381  4atexlemtlw  40437  4atexlemc  40439  cdleme15  40648  cdleme17b  40657  cdleme22e  40714  cdleme22eALTN  40715  cdleme23a  40719  cdleme28a  40740  cdleme30a  40748  cdleme32e  40815  cdleme35b  40820  trlord  40939  cdlemg10  41011  cdlemg11b  41012  cdlemg17a  41031  cdlemg35  41083  tendococl  41142  tendopltp  41150  cdlemi1  41188  cdlemk11  41219  cdlemk5u  41231  cdlemk11u  41241  cdlemk52  41324  dialss  41416  diaglbN  41425  diaintclN  41428  dia2dimlem1  41434  cdlemm10N  41488  djajN  41507  dibglbN  41536  dibintclN  41537  diblss  41540  cdlemn10  41576  dihord1  41588  dihord2pre2  41596  dihopelvalcpre  41618  dihord5apre  41632  dihmeetlem1N  41660  dihglblem2N  41664  dihmeetlem2N  41669  dihglbcpreN  41670  dihmeetlem3N  41675