Theorem lattrd 18625

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   class class class wbr 5102  ‘cfv 6538  Basecbs 17392  lecple 17440  Latclat 18610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-dm 5660  df-iota 6494  df-fv 6546  df-poset 18492  df-lat 18611

This theorem is used by:  latmlej11  18657  latjass  18662  lubun  18694  cvlcvr1  40489  exatleN  40554  2atjm  40595  2llnmat  40674  llnmlplnN  40689  2llnjaN  40716  2lplnja  40769  dalem5  40817  lncmp  40933  2lnat  40934  2llnma1b  40936  cdlema1N  40941  paddasslem5  40974  paddasslem12  40981  paddasslem13  40982  dalawlem3  41023  dalawlem5  41025  dalawlem6  41026  dalawlem7  41027  dalawlem8  41028  dalawlem11  41031  dalawlem12  41032  pl42lem1N  41129  lhpexle2lem  41159  lhpexle3lem  41161  4atexlemtlw  41217  4atexlemc  41219  cdleme15  41428  cdleme17b  41437  cdleme22e  41494  cdleme22eALTN  41495  cdleme23a  41499  cdleme28a  41520  cdleme30a  41528  cdleme32e  41595  cdleme35b  41600  trlord  41719  cdlemg10  41791  cdlemg11b  41792  cdlemg17a  41811  cdlemg35  41863  tendococl  41922  tendopltp  41930  cdlemi1  41968  cdlemk11  41999  cdlemk5u  42011  cdlemk11u  42021  cdlemk52  42104  dialss  42196  diaglbN  42205  diaintclN  42208  dia2dimlem1  42214  cdlemm10N  42268  djajN  42287  dibglbN  42316  dibintclN  42317  diblss  42320  cdlemn10  42356  dihord1  42368  dihord2pre2  42376  dihopelvalcpre  42398  dihord5apre  42412  dihmeetlem1N  42440  dihglblem2N  42444  dihmeetlem2N  42449  dihglbcpreN  42450  dihmeetlem3N  42455