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

Theorem lattrd 15890
Description: A lattice ordering is transitive. Deduction version of lattr 15888. (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 15888 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
103, 4, 5, 6, 9syl13anc 1228 . 2  |-  ( ph  ->  ( ( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
111, 2, 10mp2and 677 1  |-  ( ph  ->  X  .<_  Z )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398    e. wcel 1823   class class class wbr 4439   ` cfv 5570   Basecbs 14719   lecple 14794   Latclat 15877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-xp 4994  df-dm 4998  df-iota 5534  df-fv 5578  df-poset 15777  df-lat 15878
This theorem is referenced by:  latmlej11  15922  latjass  15927  lubun  15955  cvlcvr1  35480  exatleN  35544  2atjm  35585  2llnmat  35664  llnmlplnN  35679  2llnjaN  35706  2lplnja  35759  dalem5  35807  lncmp  35923  2lnat  35924  2llnma1b  35926  cdlema1N  35931  paddasslem5  35964  paddasslem12  35971  paddasslem13  35972  dalawlem3  36013  dalawlem5  36015  dalawlem6  36016  dalawlem7  36017  dalawlem8  36018  dalawlem11  36021  dalawlem12  36022  pl42lem1N  36119  lhpexle2lem  36149  lhpexle3lem  36151  4atexlemtlw  36207  4atexlemc  36209  cdleme15  36419  cdleme17b  36428  cdleme22e  36486  cdleme22eALTN  36487  cdleme23a  36491  cdleme28a  36512  cdleme30a  36520  cdleme32e  36587  cdleme35b  36592  trlord  36711  cdlemg10  36783  cdlemg11b  36784  cdlemg17a  36803  cdlemg35  36855  tendococl  36914  tendopltp  36922  cdlemi1  36960  cdlemk11  36991  cdlemk5u  37003  cdlemk11u  37013  cdlemk52  37096  dialss  37189  diaglbN  37198  diaintclN  37201  dia2dimlem1  37207  cdlemm10N  37261  djajN  37280  dibglbN  37309  dibintclN  37310  diblss  37313  cdlemn10  37349  dihord1  37361  dihord2pre2  37369  dihopelvalcpre  37391  dihord5apre  37405  dihmeetlem1N  37433  dihglblem2N  37437  dihmeetlem2N  37442  dihglbcpreN  37443  dihmeetlem3N  37448
  Copyright terms: Public domain W3C validator