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

Theorem latjcl 14156
Description: Closure of join operation in a lattice. (chjcom 22085 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 2283 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14154 . 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 1623    e. wcel 1684   ` cfv 5255  (class class class)co 5858   Basecbs 13148   joincjn 14078   meetcmee 14079   Latclat 14151
This theorem is referenced by:  latjcom  14165  latlej1  14166  latlej2  14167  latjle12  14168  latleeqj1  14169  latjlej1  14171  latjlej12  14173  latnlej2  14177  latjidm  14180  latnle  14191  latabs2  14194  latledi  14195  latmlej11  14196  latjass  14201  latj13  14204  latj31  14205  latj4  14207  mod1ile  14211  mod2ile  14212  lubun  14227  latdisdlem  14292  lubunNEW  28536  oldmm1  28780  olj01  28788  latmassOLD  28792  omllaw5N  28810  cmtcomlemN  28811  cmtbr2N  28816  cmtbr3N  28817  cmtbr4N  28818  lecmtN  28819  omlfh1N  28821  omlfh3N  28822  omlmod1i2N  28823  cvlexchb1  28893  cvlcvr1  28902  hlatjcl  28929  exatleN  28966  cvrval3  28975  cvrexchlem  28981  cvrexch  28982  cvratlem  28983  cvrat  28984  lnnat  28989  cvrat2  28991  atcvrj2b  28994  atltcvr  28997  atlelt  29000  2atlt  29001  atexchcvrN  29002  cvrat3  29004  cvrat4  29005  2atjm  29007  4noncolr3  29015  athgt  29018  3dim0  29019  3dimlem4a  29025  1cvratex  29035  1cvrjat  29037  1cvrat  29038  ps-2  29040  3atlem1  29045  3atlem2  29046  3at  29052  2atm  29089  lplni2  29099  lplnle  29102  2llnmj  29122  2atmat  29123  lplnexllnN  29126  2llnjaN  29128  lvoli3  29139  islvol5  29141  lvoli2  29143  lvolnle3at  29144  3atnelvolN  29148  islvol2aN  29154  4atlem3  29158  4atlem4d  29164  4atlem9  29165  4atlem10a  29166  4atlem10  29168  4atlem11a  29169  4atlem11b  29170  4atlem11  29171  4atlem12a  29172  4atlem12b  29173  4atlem12  29174  4at  29175  lplncvrlvol2  29177  2lplnja  29181  2lplnmj  29184  dalem5  29229  dalem8  29232  dalem-cly  29233  dalem38  29272  dalem39  29273  dalem44  29278  dalem54  29288  linepsubN  29314  pmapsub  29330  isline2  29336  linepmap  29337  isline3  29338  lncvrelatN  29343  2llnma1b  29348  cdlema1N  29353  cdlemblem  29355  cdlemb  29356  paddasslem5  29386  paddasslem12  29393  paddasslem13  29394  pmapjoin  29414  pmapjat1  29415  pmapjlln1  29417  hlmod1i  29418  llnmod1i2  29422  atmod2i1  29423  atmod2i2  29424  llnmod2i2  29425  atmod3i1  29426  atmod3i2  29427  dalawlem2  29434  dalawlem3  29435  dalawlem5  29437  dalawlem6  29438  dalawlem7  29439  dalawlem8  29440  dalawlem11  29443  dalawlem12  29444  pmapocjN  29492  paddatclN  29511  linepsubclN  29513  pl42lem1N  29541  pl42lem2N  29542  pl42N  29545  lhp2lt  29563  lhpj1  29584  lhpmod2i2  29600  lhpmod6i1  29601  4atexlemc  29631  lautj  29655  trlval2  29725  trlcl  29726  trljat1  29728  trljat2  29729  trlle  29746  cdlemc1  29753  cdlemc2  29754  cdlemc5  29757  cdlemd2  29761  cdlemd3  29762  cdleme0aa  29772  cdleme0b  29774  cdleme0c  29775  cdleme0cp  29776  cdleme0cq  29777  cdleme0fN  29780  cdleme1b  29788  cdleme1  29789  cdleme2  29790  cdleme3b  29791  cdleme3c  29792  cdleme4a  29801  cdleme5  29802  cdleme7e  29809  cdleme8  29812  cdleme9  29815  cdleme10  29816  cdleme11fN  29826  cdleme11g  29827  cdleme11k  29830  cdleme11  29832  cdleme15b  29837  cdleme15  29840  cdleme22gb  29856  cdleme19b  29866  cdleme20d  29874  cdleme20j  29880  cdleme20l  29884  cdleme20m  29885  cdleme22e  29906  cdleme22eALTN  29907  cdleme22f  29908  cdleme23b  29912  cdleme23c  29913  cdleme28a  29932  cdleme28b  29933  cdleme29ex  29936  cdleme30a  29940  cdlemefr29exN  29964  cdleme32e  30007  cdleme35fnpq  30011  cdleme35b  30012  cdleme35c  30013  cdleme42e  30041  cdleme42i  30045  cdleme42mgN  30050  cdlemg2fv2  30162  cdlemg7fvbwN  30169  cdlemg4c  30174  cdlemg6c  30182  cdlemg10  30203  cdlemg11b  30204  cdlemg31a  30259  cdlemg31b  30260  cdlemg35  30275  trlcolem  30288  cdlemg44a  30293  trljco  30302  tendopltp  30342  cdlemh1  30377  cdlemh2  30378  cdlemi1  30380  cdlemi  30382  cdlemk4  30396  cdlemkvcl  30404  cdlemk10  30405  cdlemk11  30411  cdlemk11u  30433  cdlemk37  30476  cdlemkid1  30484  cdlemk50  30514  cdlemk51  30515  cdlemk52  30516  dialss  30609  dia2dimlem2  30628  dia2dimlem3  30629  cdlemm10N  30681  docaclN  30687  doca2N  30689  djajN  30700  diblss  30733  cdlemn2  30758  cdlemn10  30769  dihord1  30781  dihord2pre2  30789  dihord5apre  30825  dihjatc1  30874  dihmeetlem10N  30879  dihmeetlem11N  30880  djhljjN  30965  djhj  30967  dihprrnlem1N  30987  dihprrnlem2  30988  dihjat6  30997  dihjat5N  31000  dvh4dimat  31001
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-lat 14152
  Copyright terms: Public domain W3C validator