Theorem lattrd 18403

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6492  Basecbs 17170  lecple 17218  Latclat 18388

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-dm 5634  df-iota 6448  df-fv 6500  df-poset 18270  df-lat 18389

This theorem is referenced by:  latmlej11  18435  latjass  18440  lubun  18472  cvlcvr1  39799  exatleN  39864  2atjm  39905  2llnmat  39984  llnmlplnN  39999  2llnjaN  40026  2lplnja  40079  dalem5  40127  lncmp  40243  2lnat  40244  2llnma1b  40246  cdlema1N  40251  paddasslem5  40284  paddasslem12  40291  paddasslem13  40292  dalawlem3  40333  dalawlem5  40335  dalawlem6  40336  dalawlem7  40337  dalawlem8  40338  dalawlem11  40341  dalawlem12  40342  pl42lem1N  40439  lhpexle2lem  40469  lhpexle3lem  40471  4atexlemtlw  40527  4atexlemc  40529  cdleme15  40738  cdleme17b  40747  cdleme22e  40804  cdleme22eALTN  40805  cdleme23a  40809  cdleme28a  40830  cdleme30a  40838  cdleme32e  40905  cdleme35b  40910  trlord  41029  cdlemg10  41101  cdlemg11b  41102  cdlemg17a  41121  cdlemg35  41173  tendococl  41232  tendopltp  41240  cdlemi1  41278  cdlemk11  41309  cdlemk5u  41321  cdlemk11u  41331  cdlemk52  41414  dialss  41506  diaglbN  41515  diaintclN  41518  dia2dimlem1  41524  cdlemm10N  41578  djajN  41597  dibglbN  41626  dibintclN  41627  diblss  41630  cdlemn10  41666  dihord1  41678  dihord2pre2  41686  dihopelvalcpre  41708  dihord5apre  41722  dihmeetlem1N  41750  dihglblem2N  41754  dihmeetlem2N  41759  dihglbcpreN  41760  dihmeetlem3N  41765