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

Theorem lattrd 14446
Description: A lattice ordering is transitive. Deduction version of lattr 14444. (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 14444 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
103, 4, 5, 6, 9syl13anc 1186 . 2  |-  ( ph  ->  ( ( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
111, 2, 10mp2and 661 1  |-  ( ph  ->  X  .<_  Z )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   class class class wbr 4176   ` cfv 5417   Basecbs 13428   lecple 13495   Latclat 14433
This theorem is referenced by:  latmlej11  14478  latjass  14483  lubun  14509  lubunNEW  29460  cvlcvr1  29826  exatleN  29890  2atjm  29931  2llnmat  30010  llnmlplnN  30025  2llnjaN  30052  2lplnja  30105  dalem5  30153  lncmp  30269  2lnat  30270  2llnma1b  30272  cdlema1N  30277  paddasslem5  30310  paddasslem12  30317  paddasslem13  30318  dalawlem3  30359  dalawlem5  30361  dalawlem6  30362  dalawlem7  30363  dalawlem8  30364  dalawlem11  30367  dalawlem12  30368  pl42lem1N  30465  lhpexle2lem  30495  lhpexle3lem  30497  4atexlemtlw  30553  4atexlemc  30555  cdleme15  30764  cdleme17b  30773  cdleme22e  30830  cdleme22eALTN  30831  cdleme23a  30835  cdleme28a  30856  cdleme30a  30864  cdleme32e  30931  cdleme35b  30936  trlord  31055  cdlemg10  31127  cdlemg11b  31128  cdlemg17a  31147  cdlemg35  31199  tendococl  31258  tendopltp  31266  cdlemi1  31304  cdlemk11  31335  cdlemk5u  31347  cdlemk11u  31357  cdlemk52  31440  dialss  31533  diaglbN  31542  diaintclN  31545  dia2dimlem1  31551  cdlemm10N  31605  djajN  31624  dibglbN  31653  dibintclN  31654  diblss  31657  cdlemn10  31693  dihord1  31705  dihord2pre2  31713  dihopelvalcpre  31735  dihord5apre  31749  dihmeetlem1N  31777  dihglblem2N  31781  dihmeetlem2N  31786  dihglbcpreN  31787  dihmeetlem3N  31792
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-nul 4302
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425  df-ov 6047  df-poset 14362  df-lat 14434
  Copyright terms: Public domain W3C validator