Theorem lattrd 18370

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   class class class wbr 5095  ‘cfv 6486  Basecbs 17138  lecple 17186  Latclat 18355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-dm 5633  df-iota 6442  df-fv 6494  df-poset 18237  df-lat 18356

This theorem is referenced by:  latmlej11  18402  latjass  18407  lubun  18439  cvlcvr1  39317  exatleN  39383  2atjm  39424  2llnmat  39503  llnmlplnN  39518  2llnjaN  39545  2lplnja  39598  dalem5  39646  lncmp  39762  2lnat  39763  2llnma1b  39765  cdlema1N  39770  paddasslem5  39803  paddasslem12  39810  paddasslem13  39811  dalawlem3  39852  dalawlem5  39854  dalawlem6  39855  dalawlem7  39856  dalawlem8  39857  dalawlem11  39860  dalawlem12  39861  pl42lem1N  39958  lhpexle2lem  39988  lhpexle3lem  39990  4atexlemtlw  40046  4atexlemc  40048  cdleme15  40257  cdleme17b  40266  cdleme22e  40323  cdleme22eALTN  40324  cdleme23a  40328  cdleme28a  40349  cdleme30a  40357  cdleme32e  40424  cdleme35b  40429  trlord  40548  cdlemg10  40620  cdlemg11b  40621  cdlemg17a  40640  cdlemg35  40692  tendococl  40751  tendopltp  40759  cdlemi1  40797  cdlemk11  40828  cdlemk5u  40840  cdlemk11u  40850  cdlemk52  40933  dialss  41025  diaglbN  41034  diaintclN  41037  dia2dimlem1  41043  cdlemm10N  41097  djajN  41116  dibglbN  41145  dibintclN  41146  diblss  41149  cdlemn10  41185  dihord1  41197  dihord2pre2  41205  dihopelvalcpre  41227  dihord5apre  41241  dihmeetlem1N  41269  dihglblem2N  41273  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetlem3N  41284