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

Theorem latjcl 14366
Description: Closure of join operation in a lattice. (chjcom 22519 analog.) (Contributed by NM, 14-Sep-2011.)
Hypotheses
Ref Expression
latjcl.b  |-  B  =  ( Base `  K
)
latjcl.j  |-  .\/  =  ( join `  K )
Assertion
Ref Expression
latjcl  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )

Proof of Theorem latjcl
StepHypRef Expression
1 latjcl.b . . 3  |-  B  =  ( Base `  K
)
2 latjcl.j . . 3  |-  .\/  =  ( join `  K )
3 eqid 2366 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14364 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X  .\/  Y )  e.  B  /\  ( X ( meet `  K
) Y )  e.  B ) )
54simpld 445 1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 935    = wceq 1647    e. wcel 1715   ` cfv 5358  (class class class)co 5981   Basecbs 13356   joincjn 14288   meetcmee 14289   Latclat 14361
This theorem is referenced by:  latjcom  14375  latlej1  14376  latlej2  14377  latjle12  14378  latleeqj1  14379  latjlej1  14381  latjlej12  14383  latnlej2  14387  latjidm  14390  latnle  14401  latabs2  14404  latledi  14405  latmlej11  14406  latjass  14411  latj13  14414  latj31  14415  latj4  14417  mod1ile  14421  mod2ile  14422  lubun  14437  latdisdlem  14502  lubunNEW  29222  oldmm1  29466  olj01  29474  latmassOLD  29478  omllaw5N  29496  cmtcomlemN  29497  cmtbr2N  29502  cmtbr3N  29503  cmtbr4N  29504  lecmtN  29505  omlfh1N  29507  omlfh3N  29508  omlmod1i2N  29509  cvlexchb1  29579  cvlcvr1  29588  hlatjcl  29615  exatleN  29652  cvrval3  29661  cvrexchlem  29667  cvrexch  29668  cvratlem  29669  cvrat  29670  lnnat  29675  cvrat2  29677  atcvrj2b  29680  atltcvr  29683  atlelt  29686  2atlt  29687  atexchcvrN  29688  cvrat3  29690  cvrat4  29691  2atjm  29693  4noncolr3  29701  athgt  29704  3dim0  29705  3dimlem4a  29711  1cvratex  29721  1cvrjat  29723  1cvrat  29724  ps-2  29726  3atlem1  29731  3atlem2  29732  3at  29738  2atm  29775  lplni2  29785  lplnle  29788  2llnmj  29808  2atmat  29809  lplnexllnN  29812  2llnjaN  29814  lvoli3  29825  islvol5  29827  lvoli2  29829  lvolnle3at  29830  3atnelvolN  29834  islvol2aN  29840  4atlem3  29844  4atlem4d  29850  4atlem9  29851  4atlem10a  29852  4atlem10  29854  4atlem11a  29855  4atlem11b  29856  4atlem11  29857  4atlem12a  29858  4atlem12b  29859  4atlem12  29860  4at  29861  lplncvrlvol2  29863  2lplnja  29867  2lplnmj  29870  dalem5  29915  dalem8  29918  dalem-cly  29919  dalem38  29958  dalem39  29959  dalem44  29964  dalem54  29974  linepsubN  30000  pmapsub  30016  isline2  30022  linepmap  30023  isline3  30024  lncvrelatN  30029  2llnma1b  30034  cdlema1N  30039  cdlemblem  30041  cdlemb  30042  paddasslem5  30072  paddasslem12  30079  paddasslem13  30080  pmapjoin  30100  pmapjat1  30101  pmapjlln1  30103  hlmod1i  30104  llnmod1i2  30108  atmod2i1  30109  atmod2i2  30110  llnmod2i2  30111  atmod3i1  30112  atmod3i2  30113  dalawlem2  30120  dalawlem3  30121  dalawlem5  30123  dalawlem6  30124  dalawlem7  30125  dalawlem8  30126  dalawlem11  30129  dalawlem12  30130  pmapocjN  30178  paddatclN  30197  linepsubclN  30199  pl42lem1N  30227  pl42lem2N  30228  pl42N  30231  lhp2lt  30249  lhpj1  30270  lhpmod2i2  30286  lhpmod6i1  30287  4atexlemc  30317  lautj  30341  trlval2  30411  trlcl  30412  trljat1  30414  trljat2  30415  trlle  30432  cdlemc1  30439  cdlemc2  30440  cdlemc5  30443  cdlemd2  30447  cdlemd3  30448  cdleme0aa  30458  cdleme0b  30460  cdleme0c  30461  cdleme0cp  30462  cdleme0cq  30463  cdleme0fN  30466  cdleme1b  30474  cdleme1  30475  cdleme2  30476  cdleme3b  30477  cdleme3c  30478  cdleme4a  30487  cdleme5  30488  cdleme7e  30495  cdleme8  30498  cdleme9  30501  cdleme10  30502  cdleme11fN  30512  cdleme11g  30513  cdleme11k  30516  cdleme11  30518  cdleme15b  30523  cdleme15  30526  cdleme22gb  30542  cdleme19b  30552  cdleme20d  30560  cdleme20j  30566  cdleme20l  30570  cdleme20m  30571  cdleme22e  30592  cdleme22eALTN  30593  cdleme22f  30594  cdleme23b  30598  cdleme23c  30599  cdleme28a  30618  cdleme28b  30619  cdleme29ex  30622  cdleme30a  30626  cdlemefr29exN  30650  cdleme32e  30693  cdleme35fnpq  30697  cdleme35b  30698  cdleme35c  30699  cdleme42e  30727  cdleme42i  30731  cdleme42mgN  30736  cdlemg2fv2  30848  cdlemg7fvbwN  30855  cdlemg4c  30860  cdlemg6c  30868  cdlemg10  30889  cdlemg11b  30890  cdlemg31a  30945  cdlemg31b  30946  cdlemg35  30961  trlcolem  30974  cdlemg44a  30979  trljco  30988  tendopltp  31028  cdlemh1  31063  cdlemh2  31064  cdlemi1  31066  cdlemi  31068  cdlemk4  31082  cdlemkvcl  31090  cdlemk10  31091  cdlemk11  31097  cdlemk11u  31119  cdlemk37  31162  cdlemkid1  31170  cdlemk50  31200  cdlemk51  31201  cdlemk52  31202  dialss  31295  dia2dimlem2  31314  dia2dimlem3  31315  cdlemm10N  31367  docaclN  31373  doca2N  31375  djajN  31386  diblss  31419  cdlemn2  31444  cdlemn10  31455  dihord1  31467  dihord2pre2  31475  dihord5apre  31511  dihjatc1  31560  dihmeetlem10N  31565  dihmeetlem11N  31566  djhljjN  31651  djhj  31653  dihprrnlem1N  31673  dihprrnlem2  31674  dihjat6  31683  dihjat5N  31686  dvh4dimat  31687
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984  df-lat 14362
  Copyright terms: Public domain W3C validator