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

Theorem lattr 17978
Description: A lattice ordering is transitive. (sstr 3924 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 17972 . 2 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
2 latref.b . . 3 𝐵 = (Base‘𝐾)
3 latref.l . . 3 = (le‘𝐾)
42, 3postr 17855 . 2 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
51, 4sylan 583 1 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2111   class class class wbr 5068  cfv 6398  Basecbs 16788  lecple 16837  Posetcpo 17842  Latclat 17965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-nul 5214
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3423  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-if 4455  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4835  df-br 5069  df-opab 5131  df-xp 5572  df-dm 5576  df-iota 6356  df-fv 6406  df-poset 17848  df-lat 17966
This theorem is referenced by:  lattrd  17980  latjlej1  17987  latjlej12  17989  latnlej2  17993  latmlem1  18003  latmlem12  18005  clatleglb  18052  lecmtN  37037  hlrelat2  37184  ps-2  37259  dalem3  37445  dalem17  37461  dalem21  37475  dalem25  37479  linepsubN  37533  pmapsub  37549  cdlemblem  37574  pmapjoin  37633  lhpmcvr4N  37807  4atexlemnclw  37851  cdlemd3  37981  cdleme3g  38015  cdleme3h  38016  cdleme7d  38027  cdleme21c  38108  cdleme32b  38223  cdleme35fnpq  38230  cdleme35f  38235  cdleme48bw  38283  cdlemf1  38342  cdlemg2fv2  38381  cdlemg7fvbwN  38388  cdlemg4  38398  cdlemg6c  38401  cdlemg27a  38473  cdlemg33b0  38482  cdlemg33a  38487  cdlemk3  38614  dia2dimlem1  38845  dihord6b  39041  dihord5apre  39043  dihglbcpreN  39081
  Copyright terms: Public domain W3C validator