Theorem lattrd 17539

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1508   ∈ wcel 2051   class class class wbr 4926  ‘cfv 6186  Basecbs 16338  lecple 16427  Latclat 17526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745  ax-nul 5064

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-xp 5410  df-dm 5414  df-iota 6150  df-fv 6194  df-poset 17427  df-lat 17527

This theorem is referenced by:  latmlej11  17571  latjass  17576  lubun  17604  cvlcvr1  35953  exatleN  36018  2atjm  36059  2llnmat  36138  llnmlplnN  36153  2llnjaN  36180  2lplnja  36233  dalem5  36281  lncmp  36397  2lnat  36398  2llnma1b  36400  cdlema1N  36405  paddasslem5  36438  paddasslem12  36445  paddasslem13  36446  dalawlem3  36487  dalawlem5  36489  dalawlem6  36490  dalawlem7  36491  dalawlem8  36492  dalawlem11  36495  dalawlem12  36496  pl42lem1N  36593  lhpexle2lem  36623  lhpexle3lem  36625  4atexlemtlw  36681  4atexlemc  36683  cdleme15  36892  cdleme17b  36901  cdleme22e  36958  cdleme22eALTN  36959  cdleme23a  36963  cdleme28a  36984  cdleme30a  36992  cdleme32e  37059  cdleme35b  37064  trlord  37183  cdlemg10  37255  cdlemg11b  37256  cdlemg17a  37275  cdlemg35  37327  tendococl  37386  tendopltp  37394  cdlemi1  37432  cdlemk11  37463  cdlemk5u  37475  cdlemk11u  37485  cdlemk52  37568  dialss  37660  diaglbN  37669  diaintclN  37672  dia2dimlem1  37678  cdlemm10N  37732  djajN  37751  dibglbN  37780  dibintclN  37781  diblss  37784  cdlemn10  37820  dihord1  37832  dihord2pre2  37840  dihopelvalcpre  37862  dihord5apre  37876  dihmeetlem1N  37904  dihglblem2N  37908  dihmeetlem2N  37913  dihglbcpreN  37914  dihmeetlem3N  37919