Theorem lattrd 18349

Description: A lattice ordering is transitive. Deduction version of lattr 18347. (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 18347	. . 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 2111   class class class wbr 5091  ‘cfv 6481  Basecbs 17117  lecple 17165  Latclat 18334

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-xp 5622  df-dm 5626  df-iota 6437  df-fv 6489  df-poset 18216  df-lat 18335

This theorem is referenced by:  latmlej11  18381  latjass  18386  lubun  18418  cvlcvr1  39377  exatleN  39442  2atjm  39483  2llnmat  39562  llnmlplnN  39577  2llnjaN  39604  2lplnja  39657  dalem5  39705  lncmp  39821  2lnat  39822  2llnma1b  39824  cdlema1N  39829  paddasslem5  39862  paddasslem12  39869  paddasslem13  39870  dalawlem3  39911  dalawlem5  39913  dalawlem6  39914  dalawlem7  39915  dalawlem8  39916  dalawlem11  39919  dalawlem12  39920  pl42lem1N  40017  lhpexle2lem  40047  lhpexle3lem  40049  4atexlemtlw  40105  4atexlemc  40107  cdleme15  40316  cdleme17b  40325  cdleme22e  40382  cdleme22eALTN  40383  cdleme23a  40387  cdleme28a  40408  cdleme30a  40416  cdleme32e  40483  cdleme35b  40488  trlord  40607  cdlemg10  40679  cdlemg11b  40680  cdlemg17a  40699  cdlemg35  40751  tendococl  40810  tendopltp  40818  cdlemi1  40856  cdlemk11  40887  cdlemk5u  40899  cdlemk11u  40909  cdlemk52  40992  dialss  41084  diaglbN  41093  diaintclN  41096  dia2dimlem1  41102  cdlemm10N  41156  djajN  41175  dibglbN  41204  dibintclN  41205  diblss  41208  cdlemn10  41244  dihord1  41256  dihord2pre2  41264  dihopelvalcpre  41286  dihord5apre  41300  dihmeetlem1N  41328  dihglblem2N  41332  dihmeetlem2N  41337  dihglbcpreN  41338  dihmeetlem3N  41343