Theorem lattrd 18503

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   class class class wbr 5110  ‘cfv 6538  Basecbs 17270  lecple 17318  Latclat 18488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-dm 5673  df-iota 6494  df-fv 6546  df-poset 18370  df-lat 18489

This theorem is referenced by:  latmlej11  18535  latjass  18540  lubun  18572  cvlcvr1  40094  exatleN  40159  2atjm  40200  2llnmat  40279  llnmlplnN  40294  2llnjaN  40321  2lplnja  40374  dalem5  40422  lncmp  40538  2lnat  40539  2llnma1b  40541  cdlema1N  40546  paddasslem5  40579  paddasslem12  40586  paddasslem13  40587  dalawlem3  40628  dalawlem5  40630  dalawlem6  40631  dalawlem7  40632  dalawlem8  40633  dalawlem11  40636  dalawlem12  40637  pl42lem1N  40734  lhpexle2lem  40764  lhpexle3lem  40766  4atexlemtlw  40822  4atexlemc  40824  cdleme15  41033  cdleme17b  41042  cdleme22e  41099  cdleme22eALTN  41100  cdleme23a  41104  cdleme28a  41125  cdleme30a  41133  cdleme32e  41200  cdleme35b  41205  trlord  41324  cdlemg10  41396  cdlemg11b  41397  cdlemg17a  41416  cdlemg35  41468  tendococl  41527  tendopltp  41535  cdlemi1  41573  cdlemk11  41604  cdlemk5u  41616  cdlemk11u  41626  cdlemk52  41709  dialss  41801  diaglbN  41810  diaintclN  41813  dia2dimlem1  41819  cdlemm10N  41873  djajN  41892  dibglbN  41921  dibintclN  41922  diblss  41925  cdlemn10  41961  dihord1  41973  dihord2pre2  41981  dihopelvalcpre  42003  dihord5apre  42017  dihmeetlem1N  42045  dihglblem2N  42049  dihmeetlem2N  42054  dihglbcpreN  42055  dihmeetlem3N  42060