Theorem lattrd 18468

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   class class class wbr 5097  ‘cfv 6515  Basecbs 17235  lecple 17283  Latclat 18453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-xp 5649  df-dm 5653  df-iota 6471  df-fv 6523  df-poset 18335  df-lat 18454

This theorem is referenced by:  latmlej11  18500  latjass  18505  lubun  18537  cvlcvr1  39923  exatleN  39988  2atjm  40029  2llnmat  40108  llnmlplnN  40123  2llnjaN  40150  2lplnja  40203  dalem5  40251  lncmp  40367  2lnat  40368  2llnma1b  40370  cdlema1N  40375  paddasslem5  40408  paddasslem12  40415  paddasslem13  40416  dalawlem3  40457  dalawlem5  40459  dalawlem6  40460  dalawlem7  40461  dalawlem8  40462  dalawlem11  40465  dalawlem12  40466  pl42lem1N  40563  lhpexle2lem  40593  lhpexle3lem  40595  4atexlemtlw  40651  4atexlemc  40653  cdleme15  40862  cdleme17b  40871  cdleme22e  40928  cdleme22eALTN  40929  cdleme23a  40933  cdleme28a  40954  cdleme30a  40962  cdleme32e  41029  cdleme35b  41034  trlord  41153  cdlemg10  41225  cdlemg11b  41226  cdlemg17a  41245  cdlemg35  41297  tendococl  41356  tendopltp  41364  cdlemi1  41402  cdlemk11  41433  cdlemk5u  41445  cdlemk11u  41455  cdlemk52  41538  dialss  41630  diaglbN  41639  diaintclN  41642  dia2dimlem1  41648  cdlemm10N  41702  djajN  41721  dibglbN  41750  dibintclN  41751  diblss  41754  cdlemn10  41790  dihord1  41802  dihord2pre2  41810  dihopelvalcpre  41832  dihord5apre  41846  dihmeetlem1N  41874  dihglblem2N  41878  dihmeetlem2N  41883  dihglbcpreN  41884  dihmeetlem3N  41889