Theorem lattrd 18412

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   class class class wbr 5110  ‘cfv 6514  Basecbs 17186  lecple 17234  Latclat 18397

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-dm 5651  df-iota 6467  df-fv 6522  df-poset 18281  df-lat 18398

This theorem is referenced by:  latmlej11  18444  latjass  18449  lubun  18481  cvlcvr1  39339  exatleN  39405  2atjm  39446  2llnmat  39525  llnmlplnN  39540  2llnjaN  39567  2lplnja  39620  dalem5  39668  lncmp  39784  2lnat  39785  2llnma1b  39787  cdlema1N  39792  paddasslem5  39825  paddasslem12  39832  paddasslem13  39833  dalawlem3  39874  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem11  39882  dalawlem12  39883  pl42lem1N  39980  lhpexle2lem  40010  lhpexle3lem  40012  4atexlemtlw  40068  4atexlemc  40070  cdleme15  40279  cdleme17b  40288  cdleme22e  40345  cdleme22eALTN  40346  cdleme23a  40350  cdleme28a  40371  cdleme30a  40379  cdleme32e  40446  cdleme35b  40451  trlord  40570  cdlemg10  40642  cdlemg11b  40643  cdlemg17a  40662  cdlemg35  40714  tendococl  40773  tendopltp  40781  cdlemi1  40819  cdlemk11  40850  cdlemk5u  40862  cdlemk11u  40872  cdlemk52  40955  dialss  41047  diaglbN  41056  diaintclN  41059  dia2dimlem1  41065  cdlemm10N  41119  djajN  41138  dibglbN  41167  dibintclN  41168  diblss  41171  cdlemn10  41207  dihord1  41219  dihord2pre2  41227  dihopelvalcpre  41249  dihord5apre  41263  dihmeetlem1N  41291  dihglblem2N  41295  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetlem3N  41306