Theorem lattrd 18504

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106   class class class wbr 5148  ‘cfv 6563  Basecbs 17245  lecple 17305  Latclat 18489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-dm 5699  df-iota 6516  df-fv 6571  df-poset 18371  df-lat 18490

This theorem is referenced by:  latmlej11  18536  latjass  18541  lubun  18573  cvlcvr1  39321  exatleN  39387  2atjm  39428  2llnmat  39507  llnmlplnN  39522  2llnjaN  39549  2lplnja  39602  dalem5  39650  lncmp  39766  2lnat  39767  2llnma1b  39769  cdlema1N  39774  paddasslem5  39807  paddasslem12  39814  paddasslem13  39815  dalawlem3  39856  dalawlem5  39858  dalawlem6  39859  dalawlem7  39860  dalawlem8  39861  dalawlem11  39864  dalawlem12  39865  pl42lem1N  39962  lhpexle2lem  39992  lhpexle3lem  39994  4atexlemtlw  40050  4atexlemc  40052  cdleme15  40261  cdleme17b  40270  cdleme22e  40327  cdleme22eALTN  40328  cdleme23a  40332  cdleme28a  40353  cdleme30a  40361  cdleme32e  40428  cdleme35b  40433  trlord  40552  cdlemg10  40624  cdlemg11b  40625  cdlemg17a  40644  cdlemg35  40696  tendococl  40755  tendopltp  40763  cdlemi1  40801  cdlemk11  40832  cdlemk5u  40844  cdlemk11u  40854  cdlemk52  40937  dialss  41029  diaglbN  41038  diaintclN  41041  dia2dimlem1  41047  cdlemm10N  41101  djajN  41120  dibglbN  41149  dibintclN  41150  diblss  41153  cdlemn10  41189  dihord1  41201  dihord2pre2  41209  dihopelvalcpre  41231  dihord5apre  41245  dihmeetlem1N  41273  dihglblem2N  41277  dihmeetlem2N  41282  dihglbcpreN  41283  dihmeetlem3N  41288