Theorem lattrd 18540

Description: A lattice ordering is transitive. Deduction version of lattr 18538. (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 18538	. . 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 1570   ∈ wcel 2145   class class class wbr 5107  ‘cfv 6537  Basecbs 17307  lecple 17355  Latclat 18525

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-xp 5665  df-dm 5669  df-iota 6493  df-fv 6545  df-poset 18407  df-lat 18526

This theorem is used by:  latmlej11  18572  latjass  18577  lubun  18609  cvlcvr1  40220  exatleN  40285  2atjm  40326  2llnmat  40405  llnmlplnN  40420  2llnjaN  40447  2lplnja  40500  dalem5  40548  lncmp  40664  2lnat  40665  2llnma1b  40667  cdlema1N  40672  paddasslem5  40705  paddasslem12  40712  paddasslem13  40713  dalawlem3  40754  dalawlem5  40756  dalawlem6  40757  dalawlem7  40758  dalawlem8  40759  dalawlem11  40762  dalawlem12  40763  pl42lem1N  40860  lhpexle2lem  40890  lhpexle3lem  40892  4atexlemtlw  40948  4atexlemc  40950  cdleme15  41159  cdleme17b  41168  cdleme22e  41225  cdleme22eALTN  41226  cdleme23a  41230  cdleme28a  41251  cdleme30a  41259  cdleme32e  41326  cdleme35b  41331  trlord  41450  cdlemg10  41522  cdlemg11b  41523  cdlemg17a  41542  cdlemg35  41594  tendococl  41653  tendopltp  41661  cdlemi1  41699  cdlemk11  41730  cdlemk5u  41742  cdlemk11u  41752  cdlemk52  41835  dialss  41927  diaglbN  41936  diaintclN  41939  dia2dimlem1  41945  cdlemm10N  41999  djajN  42018  dibglbN  42047  dibintclN  42048  diblss  42051  cdlemn10  42087  dihord1  42099  dihord2pre2  42107  dihopelvalcpre  42129  dihord5apre  42143  dihmeetlem1N  42171  dihglblem2N  42175  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetlem3N  42186