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

Theorem lattrd 14263
Description: A lattice ordering is transitive. Deduction version of lattr 14261. (Contributed by NM, 3-Sep-2012.)
Hypotheses
Ref Expression
lattrd.b  |-  B  =  ( Base `  K
)
lattrd.l  |-  .<_  =  ( le `  K )
lattrd.1  |-  ( ph  ->  K  e.  Lat )
lattrd.2  |-  ( ph  ->  X  e.  B )
lattrd.3  |-  ( ph  ->  Y  e.  B )
lattrd.4  |-  ( ph  ->  Z  e.  B )
lattrd.5  |-  ( ph  ->  X  .<_  Y )
lattrd.6  |-  ( ph  ->  Y  .<_  Z )
Assertion
Ref Expression
lattrd  |-  ( ph  ->  X  .<_  Z )

Proof of Theorem lattrd
StepHypRef Expression
1 lattrd.5 . 2  |-  ( ph  ->  X  .<_  Y )
2 lattrd.6 . 2  |-  ( ph  ->  Y  .<_  Z )
3 lattrd.1 . . 3  |-  ( ph  ->  K  e.  Lat )
4 lattrd.2 . . 3  |-  ( ph  ->  X  e.  B )
5 lattrd.3 . . 3  |-  ( ph  ->  Y  e.  B )
6 lattrd.4 . . 3  |-  ( ph  ->  Z  e.  B )
7 lattrd.b . . . 4  |-  B  =  ( Base `  K
)
8 lattrd.l . . . 4  |-  .<_  =  ( le `  K )
97, 8lattr 14261 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
103, 4, 5, 6, 9syl13anc 1184 . 2  |-  ( ph  ->  ( ( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
111, 2, 10mp2and 660 1  |-  ( ph  ->  X  .<_  Z )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710   class class class wbr 4104   ` cfv 5337   Basecbs 13245   lecple 13312   Latclat 14250
This theorem is referenced by:  latmlej11  14295  latjass  14300  lubun  14326  lubunNEW  29232  cvlcvr1  29598  exatleN  29662  2atjm  29703  2llnmat  29782  llnmlplnN  29797  2llnjaN  29824  2lplnja  29877  dalem5  29925  lncmp  30041  2lnat  30042  2llnma1b  30044  cdlema1N  30049  paddasslem5  30082  paddasslem12  30089  paddasslem13  30090  dalawlem3  30131  dalawlem5  30133  dalawlem6  30134  dalawlem7  30135  dalawlem8  30136  dalawlem11  30139  dalawlem12  30140  pl42lem1N  30237  lhpexle2lem  30267  lhpexle3lem  30269  4atexlemtlw  30325  4atexlemc  30327  cdleme15  30536  cdleme17b  30545  cdleme22e  30602  cdleme22eALTN  30603  cdleme23a  30607  cdleme28a  30628  cdleme30a  30636  cdleme32e  30703  cdleme35b  30708  trlord  30827  cdlemg10  30899  cdlemg11b  30900  cdlemg17a  30919  cdlemg35  30971  tendococl  31030  tendopltp  31038  cdlemi1  31076  cdlemk11  31107  cdlemk5u  31119  cdlemk11u  31129  cdlemk52  31212  dialss  31305  diaglbN  31314  diaintclN  31317  dia2dimlem1  31323  cdlemm10N  31377  djajN  31396  dibglbN  31425  dibintclN  31426  diblss  31429  cdlemn10  31465  dihord1  31477  dihord2pre2  31485  dihopelvalcpre  31507  dihord5apre  31521  dihmeetlem1N  31549  dihglblem2N  31553  dihmeetlem2N  31558  dihglbcpreN  31559  dihmeetlem3N  31564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-nul 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345  df-ov 5948  df-poset 14179  df-lat 14251
  Copyright terms: Public domain W3C validator