Theorem lattrd 18438

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099   class class class wbr 5148  ‘cfv 6548  Basecbs 17180  lecple 17240  Latclat 18423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5684  df-dm 5688  df-iota 6500  df-fv 6556  df-poset 18305  df-lat 18424

This theorem is referenced by:  latmlej11  18470  latjass  18475  lubun  18507  cvlcvr1  38811  exatleN  38877  2atjm  38918  2llnmat  38997  llnmlplnN  39012  2llnjaN  39039  2lplnja  39092  dalem5  39140  lncmp  39256  2lnat  39257  2llnma1b  39259  cdlema1N  39264  paddasslem5  39297  paddasslem12  39304  paddasslem13  39305  dalawlem3  39346  dalawlem5  39348  dalawlem6  39349  dalawlem7  39350  dalawlem8  39351  dalawlem11  39354  dalawlem12  39355  pl42lem1N  39452  lhpexle2lem  39482  lhpexle3lem  39484  4atexlemtlw  39540  4atexlemc  39542  cdleme15  39751  cdleme17b  39760  cdleme22e  39817  cdleme22eALTN  39818  cdleme23a  39822  cdleme28a  39843  cdleme30a  39851  cdleme32e  39918  cdleme35b  39923  trlord  40042  cdlemg10  40114  cdlemg11b  40115  cdlemg17a  40134  cdlemg35  40186  tendococl  40245  tendopltp  40253  cdlemi1  40291  cdlemk11  40322  cdlemk5u  40334  cdlemk11u  40344  cdlemk52  40427  dialss  40519  diaglbN  40528  diaintclN  40531  dia2dimlem1  40537  cdlemm10N  40591  djajN  40610  dibglbN  40639  dibintclN  40640  diblss  40643  cdlemn10  40679  dihord1  40691  dihord2pre2  40699  dihopelvalcpre  40721  dihord5apre  40735  dihmeetlem1N  40763  dihglblem2N  40767  dihmeetlem2N  40772  dihglbcpreN  40773  dihmeetlem3N  40778

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »