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

Theorem latjle12 14411
Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 22852 analog.) (Contributed by NM, 17-Sep-2011.)
Hypotheses
Ref Expression
latlej.b  |-  B  =  ( Base `  K
)
latlej.l  |-  .<_  =  ( le `  K )
latlej.j  |-  .\/  =  ( join `  K )
Assertion
Ref Expression
latjle12  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z ) )

Proof of Theorem latjle12
StepHypRef Expression
1 latlej.b . . . 4  |-  B  =  ( Base `  K
)
2 latlej.j . . . 4  |-  .\/  =  ( join `  K )
31, 2latjcl 14399 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
433adant3r3 1164 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  .\/  Y )  e.  B )
5 latpos 14398 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
6 latlej.l . . . 4  |-  .<_  =  ( le `  K )
71, 6, 2joinle 14370 . . 3  |-  ( ( K  e.  Poset  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B )  /\  ( X  .\/  Y
)  e.  B )  ->  ( ( X 
.<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z )
)
85, 7syl3an1 1217 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
)  /\  ( X  .\/  Y )  e.  B
)  ->  ( ( X  .<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z ) )
94, 8mpd3an3 1280 1  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1717   class class class wbr 4146   ` cfv 5387  (class class class)co 6013   Basecbs 13389   lecple 13456   Posetcpo 14317   joincjn 14321   Latclat 14394
This theorem is referenced by:  latleeqj1  14412  latjlej1  14414  latjidm  14423  latledi  14438  latjass  14444  mod1ile  14454  lubun  14470  lubunNEW  29139  oldmm1  29383  olj01  29391  cvlexchb1  29496  cvlcvr1  29505  hlrelat  29567  hlrelat2  29568  exatleN  29569  hlrelat3  29577  cvrexchlem  29584  cvratlem  29586  cvrat  29587  atlelt  29603  ps-1  29642  hlatexch3N  29645  hlatexch4  29646  3atlem1  29648  3atlem2  29649  lplnexllnN  29729  2llnjaN  29731  4atlem3  29761  4atlem10  29771  4atlem11b  29773  4atlem11  29774  4atlem12b  29776  4atlem12  29777  2lplnja  29784  dalem1  29824  dalem3  29829  dalem8  29835  dalem16  29844  dalem17  29845  dalem21  29859  dalem25  29863  dalem39  29876  dalem54  29891  dalem60  29897  linepsubN  29917  pmapsub  29933  lneq2at  29943  2llnma3r  29953  cdlema1N  29956  cdlemblem  29958  paddasslem5  29989  paddasslem12  29996  paddasslem13  29997  llnexchb2  30034  dalawlem3  30038  dalawlem5  30040  dalawlem8  30043  dalawlem11  30046  dalawlem12  30047  lhp2lt  30166  lhpexle2lem  30174  lhpexle3lem  30176  4atexlemtlw  30232  4atexlemnclw  30235  lautj  30258  cdlemd3  30365  cdleme3g  30399  cdleme3h  30400  cdleme7d  30411  cdleme11c  30426  cdleme15d  30442  cdleme17b  30452  cdleme19a  30468  cdleme20j  30483  cdleme21c  30492  cdleme22b  30506  cdleme22d  30508  cdleme28a  30535  cdleme35a  30613  cdleme35fnpq  30614  cdleme35b  30615  cdleme35f  30619  cdleme42c  30637  cdleme42i  30648  cdlemf1  30726  cdlemg4c  30777  cdlemg6c  30785  cdlemg8b  30793  cdlemg10  30806  cdlemg11b  30807  cdlemg13a  30816  cdlemg17a  30826  cdlemg18b  30844  cdlemg27a  30857  cdlemg33b0  30866  cdlemg35  30878  cdlemg42  30894  cdlemg46  30900  trljco  30905  tendopltp  30945  cdlemk3  30998  cdlemk10  31008  cdlemk1u  31024  cdlemk39  31081  dialss  31212  dia2dimlem1  31230  dia2dimlem10  31239  dia2dimlem12  31241  cdlemm10N  31284  djajN  31303  diblss  31336  cdlemn2  31361  dihord2pre2  31392  dib2dim  31409  dih2dimb  31410  dih2dimbALTN  31411  dihmeetlem6  31475  dihjatcclem1  31584
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-rep 4254  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-nel 2546  df-ral 2647  df-rex 2648  df-reu 2649  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-id 4432  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-oprab 6017  df-mpt2 6018  df-1st 6281  df-2nd 6282  df-undef 6472  df-riota 6478  df-poset 14323  df-lub 14351  df-join 14353  df-lat 14395
  Copyright terms: Public domain W3C validator