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

Theorem lattr 16984
Description: A lattice ordering is transitive. (sstr 3595 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 16978 . 2 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
2 latref.b . . 3 𝐵 = (Base‘𝐾)
3 latref.l . . 3 = (le‘𝐾)
42, 3postr 16881 . 2 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
51, 4sylan 488 1 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987   class class class wbr 4618  cfv 5852  Basecbs 15788  lecple 15876  Posetcpo 16868  Latclat 16973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4754
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-xp 5085  df-dm 5089  df-iota 5815  df-fv 5860  df-poset 16874  df-lat 16974
This theorem is referenced by:  lattrd  16986  latjlej1  16993  latjlej12  16995  latnlej2  16999  latmlem1  17009  latmlem12  17011  clatleglb  17054  lecmtN  34050  hlrelat2  34196  ps-2  34271  dalem3  34457  dalem17  34473  dalem21  34487  dalem25  34491  linepsubN  34545  pmapsub  34561  cdlemblem  34586  pmapjoin  34645  lhpmcvr4N  34819  4atexlemnclw  34863  cdlemd3  34994  cdleme3g  35028  cdleme3h  35029  cdleme7d  35040  cdleme21c  35122  cdleme32b  35237  cdleme35fnpq  35244  cdleme35f  35249  cdleme48bw  35297  cdlemf1  35356  cdlemg2fv2  35395  cdlemg7fvbwN  35402  cdlemg4  35412  cdlemg6c  35415  cdlemg27a  35487  cdlemg33b0  35496  cdlemg33a  35501  cdlemk3  35628  dia2dimlem1  35860  dihord6b  36056  dihord5apre  36058  dihglbcpreN  36096
  Copyright terms: Public domain W3C validator