Theorem lattrd 18354

Description: A lattice ordering is transitive. Deduction version of lattr 18352. (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 18352	. . 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 1541   ∈ wcel 2113   class class class wbr 5093  ‘cfv 6486  Basecbs 17122  lecple 17170  Latclat 18339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-dm 5629  df-iota 6442  df-fv 6494  df-poset 18221  df-lat 18340

This theorem is referenced by:  latmlej11  18386  latjass  18391  lubun  18423  cvlcvr1  39458  exatleN  39523  2atjm  39564  2llnmat  39643  llnmlplnN  39658  2llnjaN  39685  2lplnja  39738  dalem5  39786  lncmp  39902  2lnat  39903  2llnma1b  39905  cdlema1N  39910  paddasslem5  39943  paddasslem12  39950  paddasslem13  39951  dalawlem3  39992  dalawlem5  39994  dalawlem6  39995  dalawlem7  39996  dalawlem8  39997  dalawlem11  40000  dalawlem12  40001  pl42lem1N  40098  lhpexle2lem  40128  lhpexle3lem  40130  4atexlemtlw  40186  4atexlemc  40188  cdleme15  40397  cdleme17b  40406  cdleme22e  40463  cdleme22eALTN  40464  cdleme23a  40468  cdleme28a  40489  cdleme30a  40497  cdleme32e  40564  cdleme35b  40569  trlord  40688  cdlemg10  40760  cdlemg11b  40761  cdlemg17a  40780  cdlemg35  40832  tendococl  40891  tendopltp  40899  cdlemi1  40937  cdlemk11  40968  cdlemk5u  40980  cdlemk11u  40990  cdlemk52  41073  dialss  41165  diaglbN  41174  diaintclN  41177  dia2dimlem1  41183  cdlemm10N  41237  djajN  41256  dibglbN  41285  dibintclN  41286  diblss  41289  cdlemn10  41325  dihord1  41337  dihord2pre2  41345  dihopelvalcpre  41367  dihord5apre  41381  dihmeetlem1N  41409  dihglblem2N  41413  dihmeetlem2N  41418  dihglbcpreN  41419  dihmeetlem3N  41424