Theorem lattrd 18600

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6531  Basecbs 17367  lecple 17415  Latclat 18585

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-dm 5661  df-iota 6487  df-fv 6539  df-poset 18467  df-lat 18586

This theorem is used by:  latmlej11  18632  latjass  18637  lubun  18669  cvlcvr1  40364  exatleN  40429  2atjm  40470  2llnmat  40549  llnmlplnN  40564  2llnjaN  40591  2lplnja  40644  dalem5  40692  lncmp  40808  2lnat  40809  2llnma1b  40811  cdlema1N  40816  paddasslem5  40849  paddasslem12  40856  paddasslem13  40857  dalawlem3  40898  dalawlem5  40900  dalawlem6  40901  dalawlem7  40902  dalawlem8  40903  dalawlem11  40906  dalawlem12  40907  pl42lem1N  41004  lhpexle2lem  41034  lhpexle3lem  41036  4atexlemtlw  41092  4atexlemc  41094  cdleme15  41303  cdleme17b  41312  cdleme22e  41369  cdleme22eALTN  41370  cdleme23a  41374  cdleme28a  41395  cdleme30a  41403  cdleme32e  41470  cdleme35b  41475  trlord  41594  cdlemg10  41666  cdlemg11b  41667  cdlemg17a  41686  cdlemg35  41738  tendococl  41797  tendopltp  41805  cdlemi1  41843  cdlemk11  41874  cdlemk5u  41886  cdlemk11u  41896  cdlemk52  41979  dialss  42071  diaglbN  42080  diaintclN  42083  dia2dimlem1  42089  cdlemm10N  42143  djajN  42162  dibglbN  42191  dibintclN  42192  diblss  42195  cdlemn10  42231  dihord1  42243  dihord2pre2  42251  dihopelvalcpre  42273  dihord5apre  42287  dihmeetlem1N  42315  dihglblem2N  42319  dihmeetlem2N  42324  dihglbcpreN  42325  dihmeetlem3N  42330