Theorem lattrd 17660

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   class class class wbr 5030  ‘cfv 6324  Basecbs 16475  lecple 16564  Latclat 17647

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-xp 5525  df-dm 5529  df-iota 6283  df-fv 6332  df-poset 17548  df-lat 17648

This theorem is referenced by:  latmlej11  17692  latjass  17697  lubun  17725  cvlcvr1  36635  exatleN  36700  2atjm  36741  2llnmat  36820  llnmlplnN  36835  2llnjaN  36862  2lplnja  36915  dalem5  36963  lncmp  37079  2lnat  37080  2llnma1b  37082  cdlema1N  37087  paddasslem5  37120  paddasslem12  37127  paddasslem13  37128  dalawlem3  37169  dalawlem5  37171  dalawlem6  37172  dalawlem7  37173  dalawlem8  37174  dalawlem11  37177  dalawlem12  37178  pl42lem1N  37275  lhpexle2lem  37305  lhpexle3lem  37307  4atexlemtlw  37363  4atexlemc  37365  cdleme15  37574  cdleme17b  37583  cdleme22e  37640  cdleme22eALTN  37641  cdleme23a  37645  cdleme28a  37666  cdleme30a  37674  cdleme32e  37741  cdleme35b  37746  trlord  37865  cdlemg10  37937  cdlemg11b  37938  cdlemg17a  37957  cdlemg35  38009  tendococl  38068  tendopltp  38076  cdlemi1  38114  cdlemk11  38145  cdlemk5u  38157  cdlemk11u  38167  cdlemk52  38250  dialss  38342  diaglbN  38351  diaintclN  38354  dia2dimlem1  38360  cdlemm10N  38414  djajN  38433  dibglbN  38462  dibintclN  38463  diblss  38466  cdlemn10  38502  dihord1  38514  dihord2pre2  38522  dihopelvalcpre  38544  dihord5apre  38558  dihmeetlem1N  38586  dihglblem2N  38590  dihmeetlem2N  38595  dihglbcpreN  38596  dihmeetlem3N  38601