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

Theorem lattrd 14475
Description: A lattice ordering is transitive. Deduction version of lattr 14473. (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 14473 . . 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 1652    e. wcel 1725   class class class wbr 4204   ` cfv 5445   Basecbs 13457   lecple 13524   Latclat 14462
This theorem is referenced by:  latmlej11  14507  latjass  14512  lubun  14538  lubunNEW  29610  cvlcvr1  29976  exatleN  30040  2atjm  30081  2llnmat  30160  llnmlplnN  30175  2llnjaN  30202  2lplnja  30255  dalem5  30303  lncmp  30419  2lnat  30420  2llnma1b  30422  cdlema1N  30427  paddasslem5  30460  paddasslem12  30467  paddasslem13  30468  dalawlem3  30509  dalawlem5  30511  dalawlem6  30512  dalawlem7  30513  dalawlem8  30514  dalawlem11  30517  dalawlem12  30518  pl42lem1N  30615  lhpexle2lem  30645  lhpexle3lem  30647  4atexlemtlw  30703  4atexlemc  30705  cdleme15  30914  cdleme17b  30923  cdleme22e  30980  cdleme22eALTN  30981  cdleme23a  30985  cdleme28a  31006  cdleme30a  31014  cdleme32e  31081  cdleme35b  31086  trlord  31205  cdlemg10  31277  cdlemg11b  31278  cdlemg17a  31297  cdlemg35  31349  tendococl  31408  tendopltp  31416  cdlemi1  31454  cdlemk11  31485  cdlemk5u  31497  cdlemk11u  31507  cdlemk52  31590  dialss  31683  diaglbN  31692  diaintclN  31695  dia2dimlem1  31701  cdlemm10N  31755  djajN  31774  dibglbN  31803  dibintclN  31804  diblss  31807  cdlemn10  31843  dihord1  31855  dihord2pre2  31863  dihopelvalcpre  31885  dihord5apre  31899  dihmeetlem1N  31927  dihglblem2N  31931  dihmeetlem2N  31936  dihglbcpreN  31937  dihmeetlem3N  31942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-nul 4330
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5409  df-fv 5453  df-ov 6075  df-poset 14391  df-lat 14463
  Copyright terms: Public domain W3C validator