Theorem lattrd 18491

Description: A lattice ordering is transitive. Deduction version of lattr 18489. (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 18489	. . 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 2108   class class class wbr 5143  ‘cfv 6561  Basecbs 17247  lecple 17304  Latclat 18476

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-dm 5695  df-iota 6514  df-fv 6569  df-poset 18359  df-lat 18477

This theorem is referenced by:  latmlej11  18523  latjass  18528  lubun  18560  cvlcvr1  39340  exatleN  39406  2atjm  39447  2llnmat  39526  llnmlplnN  39541  2llnjaN  39568  2lplnja  39621  dalem5  39669  lncmp  39785  2lnat  39786  2llnma1b  39788  cdlema1N  39793  paddasslem5  39826  paddasslem12  39833  paddasslem13  39834  dalawlem3  39875  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem11  39883  dalawlem12  39884  pl42lem1N  39981  lhpexle2lem  40011  lhpexle3lem  40013  4atexlemtlw  40069  4atexlemc  40071  cdleme15  40280  cdleme17b  40289  cdleme22e  40346  cdleme22eALTN  40347  cdleme23a  40351  cdleme28a  40372  cdleme30a  40380  cdleme32e  40447  cdleme35b  40452  trlord  40571  cdlemg10  40643  cdlemg11b  40644  cdlemg17a  40663  cdlemg35  40715  tendococl  40774  tendopltp  40782  cdlemi1  40820  cdlemk11  40851  cdlemk5u  40863  cdlemk11u  40873  cdlemk52  40956  dialss  41048  diaglbN  41057  diaintclN  41060  dia2dimlem1  41066  cdlemm10N  41120  djajN  41139  dibglbN  41168  dibintclN  41169  diblss  41172  cdlemn10  41208  dihord1  41220  dihord2pre2  41228  dihopelvalcpre  41250  dihord5apre  41264  dihmeetlem1N  41292  dihglblem2N  41296  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetlem3N  41307