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

Theorem lattrd 14492
Description: A lattice ordering is transitive. Deduction version of lattr 14490. (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 14490 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
103, 4, 5, 6, 9syl13anc 1187 . 2  |-  ( ph  ->  ( ( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
111, 2, 10mp2and 662 1  |-  ( ph  ->  X  .<_  Z )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   class class class wbr 4215   ` cfv 5457   Basecbs 13474   lecple 13541   Latclat 14479
This theorem is referenced by:  latmlej11  14524  latjass  14529  lubun  14555  lubunNEW  29845  cvlcvr1  30211  exatleN  30275  2atjm  30316  2llnmat  30395  llnmlplnN  30410  2llnjaN  30437  2lplnja  30490  dalem5  30538  lncmp  30654  2lnat  30655  2llnma1b  30657  cdlema1N  30662  paddasslem5  30695  paddasslem12  30702  paddasslem13  30703  dalawlem3  30744  dalawlem5  30746  dalawlem6  30747  dalawlem7  30748  dalawlem8  30749  dalawlem11  30752  dalawlem12  30753  pl42lem1N  30850  lhpexle2lem  30880  lhpexle3lem  30882  4atexlemtlw  30938  4atexlemc  30940  cdleme15  31149  cdleme17b  31158  cdleme22e  31215  cdleme22eALTN  31216  cdleme23a  31220  cdleme28a  31241  cdleme30a  31249  cdleme32e  31316  cdleme35b  31321  trlord  31440  cdlemg10  31512  cdlemg11b  31513  cdlemg17a  31532  cdlemg35  31584  tendococl  31643  tendopltp  31651  cdlemi1  31689  cdlemk11  31720  cdlemk5u  31732  cdlemk11u  31742  cdlemk52  31825  dialss  31918  diaglbN  31927  diaintclN  31930  dia2dimlem1  31936  cdlemm10N  31990  djajN  32009  dibglbN  32038  dibintclN  32039  diblss  32042  cdlemn10  32078  dihord1  32090  dihord2pre2  32098  dihopelvalcpre  32120  dihord5apre  32134  dihmeetlem1N  32162  dihglblem2N  32166  dihmeetlem2N  32171  dihglbcpreN  32172  dihmeetlem3N  32177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-nul 4341
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-poset 14408  df-lat 14480
  Copyright terms: Public domain W3C validator