Theorem lattrd 18516

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573  Basecbs 17258  lecple 17318  Latclat 18501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-dm 5710  df-iota 6525  df-fv 6581  df-poset 18383  df-lat 18502

This theorem is referenced by:  latmlej11  18548  latjass  18553  lubun  18585  cvlcvr1  39295  exatleN  39361  2atjm  39402  2llnmat  39481  llnmlplnN  39496  2llnjaN  39523  2lplnja  39576  dalem5  39624  lncmp  39740  2lnat  39741  2llnma1b  39743  cdlema1N  39748  paddasslem5  39781  paddasslem12  39788  paddasslem13  39789  dalawlem3  39830  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem11  39838  dalawlem12  39839  pl42lem1N  39936  lhpexle2lem  39966  lhpexle3lem  39968  4atexlemtlw  40024  4atexlemc  40026  cdleme15  40235  cdleme17b  40244  cdleme22e  40301  cdleme22eALTN  40302  cdleme23a  40306  cdleme28a  40327  cdleme30a  40335  cdleme32e  40402  cdleme35b  40407  trlord  40526  cdlemg10  40598  cdlemg11b  40599  cdlemg17a  40618  cdlemg35  40670  tendococl  40729  tendopltp  40737  cdlemi1  40775  cdlemk11  40806  cdlemk5u  40818  cdlemk11u  40828  cdlemk52  40911  dialss  41003  diaglbN  41012  diaintclN  41015  dia2dimlem1  41021  cdlemm10N  41075  djajN  41094  dibglbN  41123  dibintclN  41124  diblss  41127  cdlemn10  41163  dihord1  41175  dihord2pre2  41183  dihopelvalcpre  41205  dihord5apre  41219  dihmeetlem1N  41247  dihglblem2N  41251  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetlem3N  41262