Theorem lattrd 18369

Description: A lattice ordering is transitive. Deduction version of lattr 18367. (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 18367	. . 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 5098  ‘cfv 6492  Basecbs 17136  lecple 17184  Latclat 18354

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 2708  ax-nul 5251

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-dm 5634  df-iota 6448  df-fv 6500  df-poset 18236  df-lat 18355

This theorem is referenced by:  latmlej11  18401  latjass  18406  lubun  18438  cvlcvr1  39595  exatleN  39660  2atjm  39701  2llnmat  39780  llnmlplnN  39795  2llnjaN  39822  2lplnja  39875  dalem5  39923  lncmp  40039  2lnat  40040  2llnma1b  40042  cdlema1N  40047  paddasslem5  40080  paddasslem12  40087  paddasslem13  40088  dalawlem3  40129  dalawlem5  40131  dalawlem6  40132  dalawlem7  40133  dalawlem8  40134  dalawlem11  40137  dalawlem12  40138  pl42lem1N  40235  lhpexle2lem  40265  lhpexle3lem  40267  4atexlemtlw  40323  4atexlemc  40325  cdleme15  40534  cdleme17b  40543  cdleme22e  40600  cdleme22eALTN  40601  cdleme23a  40605  cdleme28a  40626  cdleme30a  40634  cdleme32e  40701  cdleme35b  40706  trlord  40825  cdlemg10  40897  cdlemg11b  40898  cdlemg17a  40917  cdlemg35  40969  tendococl  41028  tendopltp  41036  cdlemi1  41074  cdlemk11  41105  cdlemk5u  41117  cdlemk11u  41127  cdlemk52  41210  dialss  41302  diaglbN  41311  diaintclN  41314  dia2dimlem1  41320  cdlemm10N  41374  djajN  41393  dibglbN  41422  dibintclN  41423  diblss  41426  cdlemn10  41462  dihord1  41474  dihord2pre2  41482  dihopelvalcpre  41504  dihord5apre  41518  dihmeetlem1N  41546  dihglblem2N  41550  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetlem3N  41561