MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lattrd Structured version   Visualization version   GIF version

Theorem lattrd 17659
Description: A lattice ordering is transitive. Deduction version of lattr 17657. (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
StepHypRef 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‘𝐾)
97, 8lattr 17657 . . 3 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
103, 4, 5, 6, 9syl13anc 1369 . 2 (𝜑 → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
111, 2, 10mp2and 698 1 (𝜑𝑋 𝑍)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2114   class class class wbr 5042  cfv 6334  Basecbs 16474  lecple 16563  Latclat 17646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-nul 5186
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-xp 5538  df-dm 5542  df-iota 6293  df-fv 6342  df-poset 17547  df-lat 17647
This theorem is referenced by:  latmlej11  17691  latjass  17696  lubun  17724  cvlcvr1  36593  exatleN  36658  2atjm  36699  2llnmat  36778  llnmlplnN  36793  2llnjaN  36820  2lplnja  36873  dalem5  36921  lncmp  37037  2lnat  37038  2llnma1b  37040  cdlema1N  37045  paddasslem5  37078  paddasslem12  37085  paddasslem13  37086  dalawlem3  37127  dalawlem5  37129  dalawlem6  37130  dalawlem7  37131  dalawlem8  37132  dalawlem11  37135  dalawlem12  37136  pl42lem1N  37233  lhpexle2lem  37263  lhpexle3lem  37265  4atexlemtlw  37321  4atexlemc  37323  cdleme15  37532  cdleme17b  37541  cdleme22e  37598  cdleme22eALTN  37599  cdleme23a  37603  cdleme28a  37624  cdleme30a  37632  cdleme32e  37699  cdleme35b  37704  trlord  37823  cdlemg10  37895  cdlemg11b  37896  cdlemg17a  37915  cdlemg35  37967  tendococl  38026  tendopltp  38034  cdlemi1  38072  cdlemk11  38103  cdlemk5u  38115  cdlemk11u  38125  cdlemk52  38208  dialss  38300  diaglbN  38309  diaintclN  38312  dia2dimlem1  38318  cdlemm10N  38372  djajN  38391  dibglbN  38420  dibintclN  38421  diblss  38424  cdlemn10  38460  dihord1  38472  dihord2pre2  38480  dihopelvalcpre  38502  dihord5apre  38516  dihmeetlem1N  38544  dihglblem2N  38548  dihmeetlem2N  38553  dihglbcpreN  38554  dihmeetlem3N  38559
  Copyright terms: Public domain W3C validator