Theorem lattrd 18405

Description: A lattice ordering is transitive. Deduction version of lattr 18403. (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 18403	. . 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 5107  ‘cfv 6511  Basecbs 17179  lecple 17227  Latclat 18390

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 5261

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-dm 5648  df-iota 6464  df-fv 6519  df-poset 18274  df-lat 18391

This theorem is referenced by:  latmlej11  18437  latjass  18442  lubun  18474  cvlcvr1  39332  exatleN  39398  2atjm  39439  2llnmat  39518  llnmlplnN  39533  2llnjaN  39560  2lplnja  39613  dalem5  39661  lncmp  39777  2lnat  39778  2llnma1b  39780  cdlema1N  39785  paddasslem5  39818  paddasslem12  39825  paddasslem13  39826  dalawlem3  39867  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem11  39875  dalawlem12  39876  pl42lem1N  39973  lhpexle2lem  40003  lhpexle3lem  40005  4atexlemtlw  40061  4atexlemc  40063  cdleme15  40272  cdleme17b  40281  cdleme22e  40338  cdleme22eALTN  40339  cdleme23a  40343  cdleme28a  40364  cdleme30a  40372  cdleme32e  40439  cdleme35b  40444  trlord  40563  cdlemg10  40635  cdlemg11b  40636  cdlemg17a  40655  cdlemg35  40707  tendococl  40766  tendopltp  40774  cdlemi1  40812  cdlemk11  40843  cdlemk5u  40855  cdlemk11u  40865  cdlemk52  40948  dialss  41040  diaglbN  41049  diaintclN  41052  dia2dimlem1  41058  cdlemm10N  41112  djajN  41131  dibglbN  41160  dibintclN  41161  diblss  41164  cdlemn10  41200  dihord1  41212  dihord2pre2  41220  dihopelvalcpre  41242  dihord5apre  41256  dihmeetlem1N  41284  dihglblem2N  41288  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetlem3N  41299