Theorem lattrd 18410

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   class class class wbr 5079  ‘cfv 6492  Basecbs 17177  lecple 17225  Latclat 18395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-dm 5635  df-iota 6448  df-fv 6500  df-poset 18277  df-lat 18396

This theorem is referenced by:  latmlej11  18442  latjass  18447  lubun  18479  cvlcvr1  39838  exatleN  39903  2atjm  39944  2llnmat  40023  llnmlplnN  40038  2llnjaN  40065  2lplnja  40118  dalem5  40166  lncmp  40282  2lnat  40283  2llnma1b  40285  cdlema1N  40290  paddasslem5  40323  paddasslem12  40330  paddasslem13  40331  dalawlem3  40372  dalawlem5  40374  dalawlem6  40375  dalawlem7  40376  dalawlem8  40377  dalawlem11  40380  dalawlem12  40381  pl42lem1N  40478  lhpexle2lem  40508  lhpexle3lem  40510  4atexlemtlw  40566  4atexlemc  40568  cdleme15  40777  cdleme17b  40786  cdleme22e  40843  cdleme22eALTN  40844  cdleme23a  40848  cdleme28a  40869  cdleme30a  40877  cdleme32e  40944  cdleme35b  40949  trlord  41068  cdlemg10  41140  cdlemg11b  41141  cdlemg17a  41160  cdlemg35  41212  tendococl  41271  tendopltp  41279  cdlemi1  41317  cdlemk11  41348  cdlemk5u  41360  cdlemk11u  41370  cdlemk52  41453  dialss  41545  diaglbN  41554  diaintclN  41557  dia2dimlem1  41563  cdlemm10N  41617  djajN  41636  dibglbN  41665  dibintclN  41666  diblss  41669  cdlemn10  41705  dihord1  41717  dihord2pre2  41725  dihopelvalcpre  41747  dihord5apre  41761  dihmeetlem1N  41789  dihglblem2N  41793  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetlem3N  41804