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

Theorem latjcl 14158
Description: Closure of join operation in a lattice. (chjcom 22087 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 2285 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14156 . 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 934    = wceq 1625    e. wcel 1686   ` cfv 5257  (class class class)co 5860   Basecbs 13150   joincjn 14080   meetcmee 14081   Latclat 14153
This theorem is referenced by:  latjcom  14167  latlej1  14168  latlej2  14169  latjle12  14170  latleeqj1  14171  latjlej1  14173  latjlej12  14175  latnlej2  14179  latjidm  14182  latnle  14193  latabs2  14196  latledi  14197  latmlej11  14198  latjass  14203  latj13  14206  latj31  14207  latj4  14209  mod1ile  14213  mod2ile  14214  lubun  14229  latdisdlem  14294  lubunNEW  29236  oldmm1  29480  olj01  29488  latmassOLD  29492  omllaw5N  29510  cmtcomlemN  29511  cmtbr2N  29516  cmtbr3N  29517  cmtbr4N  29518  lecmtN  29519  omlfh1N  29521  omlfh3N  29522  omlmod1i2N  29523  cvlexchb1  29593  cvlcvr1  29602  hlatjcl  29629  exatleN  29666  cvrval3  29675  cvrexchlem  29681  cvrexch  29682  cvratlem  29683  cvrat  29684  lnnat  29689  cvrat2  29691  atcvrj2b  29694  atltcvr  29697  atlelt  29700  2atlt  29701  atexchcvrN  29702  cvrat3  29704  cvrat4  29705  2atjm  29707  4noncolr3  29715  athgt  29718  3dim0  29719  3dimlem4a  29725  1cvratex  29735  1cvrjat  29737  1cvrat  29738  ps-2  29740  3atlem1  29745  3atlem2  29746  3at  29752  2atm  29789  lplni2  29799  lplnle  29802  2llnmj  29822  2atmat  29823  lplnexllnN  29826  2llnjaN  29828  lvoli3  29839  islvol5  29841  lvoli2  29843  lvolnle3at  29844  3atnelvolN  29848  islvol2aN  29854  4atlem3  29858  4atlem4d  29864  4atlem9  29865  4atlem10a  29866  4atlem10  29868  4atlem11a  29869  4atlem11b  29870  4atlem11  29871  4atlem12a  29872  4atlem12b  29873  4atlem12  29874  4at  29875  lplncvrlvol2  29877  2lplnja  29881  2lplnmj  29884  dalem5  29929  dalem8  29932  dalem-cly  29933  dalem38  29972  dalem39  29973  dalem44  29978  dalem54  29988  linepsubN  30014  pmapsub  30030  isline2  30036  linepmap  30037  isline3  30038  lncvrelatN  30043  2llnma1b  30048  cdlema1N  30053  cdlemblem  30055  cdlemb  30056  paddasslem5  30086  paddasslem12  30093  paddasslem13  30094  pmapjoin  30114  pmapjat1  30115  pmapjlln1  30117  hlmod1i  30118  llnmod1i2  30122  atmod2i1  30123  atmod2i2  30124  llnmod2i2  30125  atmod3i1  30126  atmod3i2  30127  dalawlem2  30134  dalawlem3  30135  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem11  30143  dalawlem12  30144  pmapocjN  30192  paddatclN  30211  linepsubclN  30213  pl42lem1N  30241  pl42lem2N  30242  pl42N  30245  lhp2lt  30263  lhpj1  30284  lhpmod2i2  30300  lhpmod6i1  30301  4atexlemc  30331  lautj  30355  trlval2  30425  trlcl  30426  trljat1  30428  trljat2  30429  trlle  30446  cdlemc1  30453  cdlemc2  30454  cdlemc5  30457  cdlemd2  30461  cdlemd3  30462  cdleme0aa  30472  cdleme0b  30474  cdleme0c  30475  cdleme0cp  30476  cdleme0cq  30477  cdleme0fN  30480  cdleme1b  30488  cdleme1  30489  cdleme2  30490  cdleme3b  30491  cdleme3c  30492  cdleme4a  30501  cdleme5  30502  cdleme7e  30509  cdleme8  30512  cdleme9  30515  cdleme10  30516  cdleme11fN  30526  cdleme11g  30527  cdleme11k  30530  cdleme11  30532  cdleme15b  30537  cdleme15  30540  cdleme22gb  30556  cdleme19b  30566  cdleme20d  30574  cdleme20j  30580  cdleme20l  30584  cdleme20m  30585  cdleme22e  30606  cdleme22eALTN  30607  cdleme22f  30608  cdleme23b  30612  cdleme23c  30613  cdleme28a  30632  cdleme28b  30633  cdleme29ex  30636  cdleme30a  30640  cdlemefr29exN  30664  cdleme32e  30707  cdleme35fnpq  30711  cdleme35b  30712  cdleme35c  30713  cdleme42e  30741  cdleme42i  30745  cdleme42mgN  30750  cdlemg2fv2  30862  cdlemg7fvbwN  30869  cdlemg4c  30874  cdlemg6c  30882  cdlemg10  30903  cdlemg11b  30904  cdlemg31a  30959  cdlemg31b  30960  cdlemg35  30975  trlcolem  30988  cdlemg44a  30993  trljco  31002  tendopltp  31042  cdlemh1  31077  cdlemh2  31078  cdlemi1  31080  cdlemi  31082  cdlemk4  31096  cdlemkvcl  31104  cdlemk10  31105  cdlemk11  31111  cdlemk11u  31133  cdlemk37  31176  cdlemkid1  31184  cdlemk50  31214  cdlemk51  31215  cdlemk52  31216  dialss  31309  dia2dimlem2  31328  dia2dimlem3  31329  cdlemm10N  31381  docaclN  31387  doca2N  31389  djajN  31400  diblss  31433  cdlemn2  31458  cdlemn10  31469  dihord1  31481  dihord2pre2  31489  dihord5apre  31525  dihjatc1  31574  dihmeetlem10N  31579  dihmeetlem11N  31580  djhljjN  31665  djhj  31667  dihprrnlem1N  31687  dihprrnlem2  31688  dihjat6  31697  dihjat5N  31700  dvh4dimat  31701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-lat 14154
  Copyright terms: Public domain W3C validator