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

Theorem lattrd 15228
Description: A lattice ordering is transitive. Deduction version of lattr 15226. (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 15226 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
103, 4, 5, 6, 9syl13anc 1220 . 2  |-  ( ph  ->  ( ( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
111, 2, 10mp2and 679 1  |-  ( ph  ->  X  .<_  Z )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   class class class wbr 4292   ` cfv 5418   Basecbs 14174   lecple 14245   Latclat 15215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-xp 4846  df-dm 4850  df-iota 5381  df-fv 5426  df-poset 15116  df-lat 15216
This theorem is referenced by:  latmlej11  15260  latjass  15265  lubun  15293  cvlcvr1  32984  exatleN  33048  2atjm  33089  2llnmat  33168  llnmlplnN  33183  2llnjaN  33210  2lplnja  33263  dalem5  33311  lncmp  33427  2lnat  33428  2llnma1b  33430  cdlema1N  33435  paddasslem5  33468  paddasslem12  33475  paddasslem13  33476  dalawlem3  33517  dalawlem5  33519  dalawlem6  33520  dalawlem7  33521  dalawlem8  33522  dalawlem11  33525  dalawlem12  33526  pl42lem1N  33623  lhpexle2lem  33653  lhpexle3lem  33655  4atexlemtlw  33711  4atexlemc  33713  cdleme15  33922  cdleme17b  33931  cdleme22e  33988  cdleme22eALTN  33989  cdleme23a  33993  cdleme28a  34014  cdleme30a  34022  cdleme32e  34089  cdleme35b  34094  trlord  34213  cdlemg10  34285  cdlemg11b  34286  cdlemg17a  34305  cdlemg35  34357  tendococl  34416  tendopltp  34424  cdlemi1  34462  cdlemk11  34493  cdlemk5u  34505  cdlemk11u  34515  cdlemk52  34598  dialss  34691  diaglbN  34700  diaintclN  34703  dia2dimlem1  34709  cdlemm10N  34763  djajN  34782  dibglbN  34811  dibintclN  34812  diblss  34815  cdlemn10  34851  dihord1  34863  dihord2pre2  34871  dihopelvalcpre  34893  dihord5apre  34907  dihmeetlem1N  34935  dihglblem2N  34939  dihmeetlem2N  34944  dihglbcpreN  34945  dihmeetlem3N  34950
  Copyright terms: Public domain W3C validator