Theorem lattrd 18490

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   class class class wbr 5104  ‘cfv 6525  Basecbs 17257  lecple 17305  Latclat 18475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5260

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-xp 5657  df-dm 5661  df-iota 6481  df-fv 6533  df-poset 18357  df-lat 18476

This theorem is referenced by:  latmlej11  18522  latjass  18527  lubun  18559  cvlcvr1  39970  exatleN  40035  2atjm  40076  2llnmat  40155  llnmlplnN  40170  2llnjaN  40197  2lplnja  40250  dalem5  40298  lncmp  40414  2lnat  40415  2llnma1b  40417  cdlema1N  40422  paddasslem5  40455  paddasslem12  40462  paddasslem13  40463  dalawlem3  40504  dalawlem5  40506  dalawlem6  40507  dalawlem7  40508  dalawlem8  40509  dalawlem11  40512  dalawlem12  40513  pl42lem1N  40610  lhpexle2lem  40640  lhpexle3lem  40642  4atexlemtlw  40698  4atexlemc  40700  cdleme15  40909  cdleme17b  40918  cdleme22e  40975  cdleme22eALTN  40976  cdleme23a  40980  cdleme28a  41001  cdleme30a  41009  cdleme32e  41076  cdleme35b  41081  trlord  41200  cdlemg10  41272  cdlemg11b  41273  cdlemg17a  41292  cdlemg35  41344  tendococl  41403  tendopltp  41411  cdlemi1  41449  cdlemk11  41480  cdlemk5u  41492  cdlemk11u  41502  cdlemk52  41585  dialss  41677  diaglbN  41686  diaintclN  41689  dia2dimlem1  41695  cdlemm10N  41749  djajN  41768  dibglbN  41797  dibintclN  41798  diblss  41801  cdlemn10  41837  dihord1  41849  dihord2pre2  41857  dihopelvalcpre  41879  dihord5apre  41893  dihmeetlem1N  41921  dihglblem2N  41925  dihmeetlem2N  41930  dihglbcpreN  41931  dihmeetlem3N  41936