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

Theorem lattr 17661
Description: A lattice ordering is transitive. (sstr 3979 analog.) (Contributed by NM, 17-Nov-2011.)
Hypotheses
Ref Expression
latref.b 𝐵 = (Base‘𝐾)
latref.l = (le‘𝐾)
Assertion
Ref Expression
lattr ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))

Proof of Theorem lattr
StepHypRef Expression
1 latpos 17655 . 2 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
2 latref.b . . 3 𝐵 = (Base‘𝐾)
3 latref.l . . 3 = (le‘𝐾)
42, 3postr 17558 . 2 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
51, 4sylan 580 1 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081   = wceq 1530  wcel 2107   class class class wbr 5063  cfv 6354  Basecbs 16478  lecple 16567  Posetcpo 17545  Latclat 17650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-nul 5207
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-xp 5560  df-dm 5564  df-iota 6313  df-fv 6362  df-poset 17551  df-lat 17651
This theorem is referenced by:  lattrd  17663  latjlej1  17670  latjlej12  17672  latnlej2  17676  latmlem1  17686  latmlem12  17688  clatleglb  17731  lecmtN  36278  hlrelat2  36425  ps-2  36500  dalem3  36686  dalem17  36702  dalem21  36716  dalem25  36720  linepsubN  36774  pmapsub  36790  cdlemblem  36815  pmapjoin  36874  lhpmcvr4N  37048  4atexlemnclw  37092  cdlemd3  37222  cdleme3g  37256  cdleme3h  37257  cdleme7d  37268  cdleme21c  37349  cdleme32b  37464  cdleme35fnpq  37471  cdleme35f  37476  cdleme48bw  37524  cdlemf1  37583  cdlemg2fv2  37622  cdlemg7fvbwN  37629  cdlemg4  37639  cdlemg6c  37642  cdlemg27a  37714  cdlemg33b0  37723  cdlemg33a  37728  cdlemk3  37855  dia2dimlem1  38086  dihord6b  38282  dihord5apre  38284  dihglbcpreN  38322
  Copyright terms: Public domain W3C validator