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

Theorem lattrd 14374
Description: A lattice ordering is transitive. Deduction version of lattr 14372. (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 14372 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
103, 4, 5, 6, 9syl13anc 1185 . 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 1647    e. wcel 1715   class class class wbr 4125   ` cfv 5358   Basecbs 13356   lecple 13423   Latclat 14361
This theorem is referenced by:  latmlej11  14406  latjass  14411  lubun  14437  lubunNEW  29234  cvlcvr1  29600  exatleN  29664  2atjm  29705  2llnmat  29784  llnmlplnN  29799  2llnjaN  29826  2lplnja  29879  dalem5  29927  lncmp  30043  2lnat  30044  2llnma1b  30046  cdlema1N  30051  paddasslem5  30084  paddasslem12  30091  paddasslem13  30092  dalawlem3  30133  dalawlem5  30135  dalawlem6  30136  dalawlem7  30137  dalawlem8  30138  dalawlem11  30141  dalawlem12  30142  pl42lem1N  30239  lhpexle2lem  30269  lhpexle3lem  30271  4atexlemtlw  30327  4atexlemc  30329  cdleme15  30538  cdleme17b  30547  cdleme22e  30604  cdleme22eALTN  30605  cdleme23a  30609  cdleme28a  30630  cdleme30a  30638  cdleme32e  30705  cdleme35b  30710  trlord  30829  cdlemg10  30901  cdlemg11b  30902  cdlemg17a  30921  cdlemg35  30973  tendococl  31032  tendopltp  31040  cdlemi1  31078  cdlemk11  31109  cdlemk5u  31121  cdlemk11u  31131  cdlemk52  31214  dialss  31307  diaglbN  31316  diaintclN  31319  dia2dimlem1  31325  cdlemm10N  31379  djajN  31398  dibglbN  31427  dibintclN  31428  diblss  31431  cdlemn10  31467  dihord1  31479  dihord2pre2  31487  dihopelvalcpre  31509  dihord5apre  31523  dihmeetlem1N  31551  dihglblem2N  31555  dihmeetlem2N  31560  dihglbcpreN  31561  dihmeetlem3N  31566
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-nul 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984  df-poset 14290  df-lat 14362
  Copyright terms: Public domain W3C validator