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

Theorem lattr 15532
Description: A lattice ordering is transitive. (sstr 3505 analog.) (Contributed by NM, 17-Nov-2011.)
Hypotheses
Ref Expression
latref.b  |-  B  =  ( Base `  K
)
latref.l  |-  .<_  =  ( le `  K )
Assertion
Ref Expression
lattr  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )

Proof of Theorem lattr
StepHypRef Expression
1 latpos 15526 . 2  |-  ( K  e.  Lat  ->  K  e.  Poset )
2 latref.b . . 3  |-  B  =  ( Base `  K
)
3 latref.l . . 3  |-  .<_  =  ( le `  K )
42, 3postr 15429 . 2  |-  ( ( K  e.  Poset  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B )
)  ->  ( ( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
51, 4sylan 471 1  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968    = wceq 1374    e. wcel 1762   class class class wbr 4440   ` cfv 5579   Basecbs 14479   lecple 14551   Posetcpo 15416   Latclat 15521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-nul 4569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-xp 4998  df-dm 5002  df-iota 5542  df-fv 5587  df-poset 15422  df-lat 15522
This theorem is referenced by:  lattrd  15534  latjlej1  15541  latjlej12  15543  latnlej2  15547  latmlem1  15557  latmlem12  15559  clatleglb  15602  lecmtN  33928  hlrelat2  34074  ps-2  34149  dalem3  34335  dalem17  34351  dalem21  34365  dalem25  34369  linepsubN  34423  pmapsub  34439  cdlemblem  34464  pmapjoin  34523  lhpmcvr4N  34697  4atexlemnclw  34741  cdlemd3  34871  cdleme3g  34905  cdleme3h  34906  cdleme7d  34917  cdleme21c  34998  cdleme32b  35113  cdleme35fnpq  35120  cdleme35f  35125  cdleme48bw  35173  cdlemf1  35232  cdlemg2fv2  35271  cdlemg7fvbwN  35278  cdlemg4  35288  cdlemg6c  35291  cdlemg27a  35363  cdlemg33b0  35372  cdlemg33a  35377  cdlemk3  35504  dia2dimlem1  35736  dihord6b  35932  dihord5apre  35934  dihglbcpreN  35972
  Copyright terms: Public domain W3C validator