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

Theorem lattrd 15534
Description: A lattice ordering is transitive. Deduction version of lattr 15532. (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 15532 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  Y  .<_  Z )  ->  X  .<_  Z ) )
103, 4, 5, 6, 9syl13anc 1225 . 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 1374    e. wcel 1762   class class class wbr 4440   ` cfv 5579   Basecbs 14479   lecple 14551   Latclat 15521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-nul 4569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-xp 4998  df-dm 5002  df-iota 5542  df-fv 5587  df-poset 15422  df-lat 15522
This theorem is referenced by:  latmlej11  15566  latjass  15571  lubun  15599  cvlcvr1  34011  exatleN  34075  2atjm  34116  2llnmat  34195  llnmlplnN  34210  2llnjaN  34237  2lplnja  34290  dalem5  34338  lncmp  34454  2lnat  34455  2llnma1b  34457  cdlema1N  34462  paddasslem5  34495  paddasslem12  34502  paddasslem13  34503  dalawlem3  34544  dalawlem5  34546  dalawlem6  34547  dalawlem7  34548  dalawlem8  34549  dalawlem11  34552  dalawlem12  34553  pl42lem1N  34650  lhpexle2lem  34680  lhpexle3lem  34682  4atexlemtlw  34738  4atexlemc  34740  cdleme15  34949  cdleme17b  34958  cdleme22e  35015  cdleme22eALTN  35016  cdleme23a  35020  cdleme28a  35041  cdleme30a  35049  cdleme32e  35116  cdleme35b  35121  trlord  35240  cdlemg10  35312  cdlemg11b  35313  cdlemg17a  35332  cdlemg35  35384  tendococl  35443  tendopltp  35451  cdlemi1  35489  cdlemk11  35520  cdlemk5u  35532  cdlemk11u  35542  cdlemk52  35625  dialss  35718  diaglbN  35727  diaintclN  35730  dia2dimlem1  35736  cdlemm10N  35790  djajN  35809  dibglbN  35838  dibintclN  35839  diblss  35842  cdlemn10  35878  dihord1  35890  dihord2pre2  35898  dihopelvalcpre  35920  dihord5apre  35934  dihmeetlem1N  35962  dihglblem2N  35966  dihmeetlem2N  35971  dihglbcpreN  35972  dihmeetlem3N  35977
  Copyright terms: Public domain W3C validator