Theorem lattrd 18527

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   class class class wbr 5114  ‘cfv 6543  Basecbs 17294  lecple 17342  Latclat 18512

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-dm 5676  df-iota 6499  df-fv 6551  df-poset 18394  df-lat 18513

This theorem is used by:  latmlej11  18559  latjass  18564  lubun  18596  cvlcvr1  40154  exatleN  40219  2atjm  40260  2llnmat  40339  llnmlplnN  40354  2llnjaN  40381  2lplnja  40434  dalem5  40482  lncmp  40598  2lnat  40599  2llnma1b  40601  cdlema1N  40606  paddasslem5  40639  paddasslem12  40646  paddasslem13  40647  dalawlem3  40688  dalawlem5  40690  dalawlem6  40691  dalawlem7  40692  dalawlem8  40693  dalawlem11  40696  dalawlem12  40697  pl42lem1N  40794  lhpexle2lem  40824  lhpexle3lem  40826  4atexlemtlw  40882  4atexlemc  40884  cdleme15  41093  cdleme17b  41102  cdleme22e  41159  cdleme22eALTN  41160  cdleme23a  41164  cdleme28a  41185  cdleme30a  41193  cdleme32e  41260  cdleme35b  41265  trlord  41384  cdlemg10  41456  cdlemg11b  41457  cdlemg17a  41476  cdlemg35  41528  tendococl  41587  tendopltp  41595  cdlemi1  41633  cdlemk11  41664  cdlemk5u  41676  cdlemk11u  41686  cdlemk52  41769  dialss  41861  diaglbN  41870  diaintclN  41873  dia2dimlem1  41879  cdlemm10N  41933  djajN  41952  dibglbN  41981  dibintclN  41982  diblss  41985  cdlemn10  42021  dihord1  42033  dihord2pre2  42041  dihopelvalcpre  42063  dihord5apre  42077  dihmeetlem1N  42105  dihglblem2N  42109  dihmeetlem2N  42114  dihglbcpreN  42115  dihmeetlem3N  42120