Theorem lattrd 17266

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145   class class class wbr 4786  ‘cfv 6031  Basecbs 16064  lecple 16156  Latclat 17253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-dm 5259  df-iota 5994  df-fv 6039  df-poset 17154  df-lat 17254

This theorem is referenced by:  latmlej11  17298  latjass  17303  lubun  17331  cvlcvr1  35148  exatleN  35212  2atjm  35253  2llnmat  35332  llnmlplnN  35347  2llnjaN  35374  2lplnja  35427  dalem5  35475  lncmp  35591  2lnat  35592  2llnma1b  35594  cdlema1N  35599  paddasslem5  35632  paddasslem12  35639  paddasslem13  35640  dalawlem3  35681  dalawlem5  35683  dalawlem6  35684  dalawlem7  35685  dalawlem8  35686  dalawlem11  35689  dalawlem12  35690  pl42lem1N  35787  lhpexle2lem  35817  lhpexle3lem  35819  4atexlemtlw  35875  4atexlemc  35877  cdleme15  36087  cdleme17b  36096  cdleme22e  36153  cdleme22eALTN  36154  cdleme23a  36158  cdleme28a  36179  cdleme30a  36187  cdleme32e  36254  cdleme35b  36259  trlord  36378  cdlemg10  36450  cdlemg11b  36451  cdlemg17a  36470  cdlemg35  36522  tendococl  36581  tendopltp  36589  cdlemi1  36627  cdlemk11  36658  cdlemk5u  36670  cdlemk11u  36680  cdlemk52  36763  dialss  36856  diaglbN  36865  diaintclN  36868  dia2dimlem1  36874  cdlemm10N  36928  djajN  36947  dibglbN  36976  dibintclN  36977  diblss  36980  cdlemn10  37016  dihord1  37028  dihord2pre2  37036  dihopelvalcpre  37058  dihord5apre  37072  dihmeetlem1N  37100  dihglblem2N  37104  dihmeetlem2N  37109  dihglbcpreN  37110  dihmeetlem3N  37115