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

Theorem lattr 15337
Description: A lattice ordering is transitive. (sstr 3465 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 15331 . 2  |-  ( K  e.  Lat  ->  K  e.  Poset )
2 latref.b . . 3  |-  B  =  ( Base `  K
)
3 latref.l . . 3  |-  .<_  =  ( le `  K )
42, 3postr 15234 . 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 965    = wceq 1370    e. wcel 1758   class class class wbr 4393   ` cfv 5519   Basecbs 14285   lecple 14356   Posetcpo 15221   Latclat 15326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-nul 4522
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-xp 4947  df-dm 4951  df-iota 5482  df-fv 5527  df-poset 15227  df-lat 15327
This theorem is referenced by:  lattrd  15339  latjlej1  15346  latjlej12  15348  latnlej2  15352  latmlem1  15362  latmlem12  15364  clatleglb  15407  lecmtN  33210  hlrelat2  33356  ps-2  33431  dalem3  33617  dalem17  33633  dalem21  33647  dalem25  33651  linepsubN  33705  pmapsub  33721  cdlemblem  33746  pmapjoin  33805  lhpmcvr4N  33979  4atexlemnclw  34023  cdlemd3  34153  cdleme3g  34187  cdleme3h  34188  cdleme7d  34199  cdleme21c  34280  cdleme32b  34395  cdleme35fnpq  34402  cdleme35f  34407  cdleme48bw  34455  cdlemf1  34514  cdlemg2fv2  34553  cdlemg7fvbwN  34560  cdlemg4  34570  cdlemg6c  34573  cdlemg27a  34645  cdlemg33b0  34654  cdlemg33a  34659  cdlemk3  34786  dia2dimlem1  35018  dihord6b  35214  dihord5apre  35216  dihglbcpreN  35254
  Copyright terms: Public domain W3C validator