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

Theorem lattrd 14166
Description: A lattice ordering is transitive. Deduction version of lattr 14164. (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 14164 . . 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 1625    e. wcel 1686   class class class wbr 4025   ` cfv 5257   Basecbs 13150   lecple 13217   Latclat 14153
This theorem is referenced by:  latmlej11  14198  latjass  14203  lubun  14229  lubunNEW  29236  cvlcvr1  29602  exatleN  29666  2atjm  29707  2llnmat  29786  llnmlplnN  29801  2llnjaN  29828  2lplnja  29881  dalem5  29929  lncmp  30045  2lnat  30046  2llnma1b  30048  cdlema1N  30053  paddasslem5  30086  paddasslem12  30093  paddasslem13  30094  dalawlem3  30135  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem11  30143  dalawlem12  30144  pl42lem1N  30241  lhpexle2lem  30271  lhpexle3lem  30273  4atexlemtlw  30329  4atexlemc  30331  cdleme15  30540  cdleme17b  30549  cdleme22e  30606  cdleme22eALTN  30607  cdleme23a  30611  cdleme28a  30632  cdleme30a  30640  cdleme32e  30707  cdleme35b  30712  trlord  30831  cdlemg10  30903  cdlemg11b  30904  cdlemg17a  30923  cdlemg35  30975  tendococl  31034  tendopltp  31042  cdlemi1  31080  cdlemk11  31111  cdlemk5u  31123  cdlemk11u  31133  cdlemk52  31216  dialss  31309  diaglbN  31318  diaintclN  31321  dia2dimlem1  31327  cdlemm10N  31381  djajN  31400  dibglbN  31429  dibintclN  31430  diblss  31433  cdlemn10  31469  dihord1  31481  dihord2pre2  31489  dihopelvalcpre  31511  dihord5apre  31525  dihmeetlem1N  31553  dihglblem2N  31557  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetlem3N  31568
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-nul 4151
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-poset 14082  df-lat 14154
  Copyright terms: Public domain W3C validator