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

Theorem latjcl 14406
Description: Closure of join operation in a lattice. (chjcom 22856 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 2387 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14404 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X  .\/  Y )  e.  B  /\  ( X ( meet `  K
) Y )  e.  B ) )
54simpld 446 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 936    = wceq 1649    e. wcel 1717   ` cfv 5394  (class class class)co 6020   Basecbs 13396   joincjn 14328   meetcmee 14329   Latclat 14401
This theorem is referenced by:  latjcom  14415  latlej1  14416  latlej2  14417  latjle12  14418  latleeqj1  14419  latjlej1  14421  latjlej12  14423  latnlej2  14427  latjidm  14430  latnle  14441  latabs2  14444  latledi  14445  latmlej11  14446  latjass  14451  latj13  14454  latj31  14455  latj4  14457  mod1ile  14461  mod2ile  14462  lubun  14477  latdisdlem  14542  lubunNEW  29088  oldmm1  29332  olj01  29340  latmassOLD  29344  omllaw5N  29362  cmtcomlemN  29363  cmtbr2N  29368  cmtbr3N  29369  cmtbr4N  29370  lecmtN  29371  omlfh1N  29373  omlfh3N  29374  omlmod1i2N  29375  cvlexchb1  29445  cvlcvr1  29454  hlatjcl  29481  exatleN  29518  cvrval3  29527  cvrexchlem  29533  cvrexch  29534  cvratlem  29535  cvrat  29536  lnnat  29541  cvrat2  29543  atcvrj2b  29546  atltcvr  29549  atlelt  29552  2atlt  29553  atexchcvrN  29554  cvrat3  29556  cvrat4  29557  2atjm  29559  4noncolr3  29567  athgt  29570  3dim0  29571  3dimlem4a  29577  1cvratex  29587  1cvrjat  29589  1cvrat  29590  ps-2  29592  3atlem1  29597  3atlem2  29598  3at  29604  2atm  29641  lplni2  29651  lplnle  29654  2llnmj  29674  2atmat  29675  lplnexllnN  29678  2llnjaN  29680  lvoli3  29691  islvol5  29693  lvoli2  29695  lvolnle3at  29696  3atnelvolN  29700  islvol2aN  29706  4atlem3  29710  4atlem4d  29716  4atlem9  29717  4atlem10a  29718  4atlem10  29720  4atlem11a  29721  4atlem11b  29722  4atlem11  29723  4atlem12a  29724  4atlem12b  29725  4atlem12  29726  4at  29727  lplncvrlvol2  29729  2lplnja  29733  2lplnmj  29736  dalem5  29781  dalem8  29784  dalem-cly  29785  dalem38  29824  dalem39  29825  dalem44  29830  dalem54  29840  linepsubN  29866  pmapsub  29882  isline2  29888  linepmap  29889  isline3  29890  lncvrelatN  29895  2llnma1b  29900  cdlema1N  29905  cdlemblem  29907  cdlemb  29908  paddasslem5  29938  paddasslem12  29945  paddasslem13  29946  pmapjoin  29966  pmapjat1  29967  pmapjlln1  29969  hlmod1i  29970  llnmod1i2  29974  atmod2i1  29975  atmod2i2  29976  llnmod2i2  29977  atmod3i1  29978  atmod3i2  29979  dalawlem2  29986  dalawlem3  29987  dalawlem5  29989  dalawlem6  29990  dalawlem7  29991  dalawlem8  29992  dalawlem11  29995  dalawlem12  29996  pmapocjN  30044  paddatclN  30063  linepsubclN  30065  pl42lem1N  30093  pl42lem2N  30094  pl42N  30097  lhp2lt  30115  lhpj1  30136  lhpmod2i2  30152  lhpmod6i1  30153  4atexlemc  30183  lautj  30207  trlval2  30277  trlcl  30278  trljat1  30280  trljat2  30281  trlle  30298  cdlemc1  30305  cdlemc2  30306  cdlemc5  30309  cdlemd2  30313  cdlemd3  30314  cdleme0aa  30324  cdleme0b  30326  cdleme0c  30327  cdleme0cp  30328  cdleme0cq  30329  cdleme0fN  30332  cdleme1b  30340  cdleme1  30341  cdleme2  30342  cdleme3b  30343  cdleme3c  30344  cdleme4a  30353  cdleme5  30354  cdleme7e  30361  cdleme8  30364  cdleme9  30367  cdleme10  30368  cdleme11fN  30378  cdleme11g  30379  cdleme11k  30382  cdleme11  30384  cdleme15b  30389  cdleme15  30392  cdleme22gb  30408  cdleme19b  30418  cdleme20d  30426  cdleme20j  30432  cdleme20l  30436  cdleme20m  30437  cdleme22e  30458  cdleme22eALTN  30459  cdleme22f  30460  cdleme23b  30464  cdleme23c  30465  cdleme28a  30484  cdleme28b  30485  cdleme29ex  30488  cdleme30a  30492  cdlemefr29exN  30516  cdleme32e  30559  cdleme35fnpq  30563  cdleme35b  30564  cdleme35c  30565  cdleme42e  30593  cdleme42i  30597  cdleme42mgN  30602  cdlemg2fv2  30714  cdlemg7fvbwN  30721  cdlemg4c  30726  cdlemg6c  30734  cdlemg10  30755  cdlemg11b  30756  cdlemg31a  30811  cdlemg31b  30812  cdlemg35  30827  trlcolem  30840  cdlemg44a  30845  trljco  30854  tendopltp  30894  cdlemh1  30929  cdlemh2  30930  cdlemi1  30932  cdlemi  30934  cdlemk4  30948  cdlemkvcl  30956  cdlemk10  30957  cdlemk11  30963  cdlemk11u  30985  cdlemk37  31028  cdlemkid1  31036  cdlemk50  31066  cdlemk51  31067  cdlemk52  31068  dialss  31161  dia2dimlem2  31180  dia2dimlem3  31181  cdlemm10N  31233  docaclN  31239  doca2N  31241  djajN  31252  diblss  31285  cdlemn2  31310  cdlemn10  31321  dihord1  31333  dihord2pre2  31341  dihord5apre  31377  dihjatc1  31426  dihmeetlem10N  31431  dihmeetlem11N  31432  djhljjN  31517  djhj  31519  dihprrnlem1N  31539  dihprrnlem2  31540  dihjat6  31549  dihjat5N  31552  dvh4dimat  31553
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-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-lat 14402
  Copyright terms: Public domain W3C validator