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

Theorem latjcl 14462
Description: Closure of join operation in a lattice. (chjcom 22991 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 2430 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14460 . 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 1652    e. wcel 1725   ` cfv 5440  (class class class)co 6067   Basecbs 13452   joincjn 14384   meetcmee 14385   Latclat 14457
This theorem is referenced by:  latjcom  14471  latlej1  14472  latlej2  14473  latjle12  14474  latleeqj1  14475  latjlej1  14477  latjlej12  14479  latnlej2  14483  latjidm  14486  latnle  14497  latabs2  14500  latledi  14501  latmlej11  14502  latjass  14507  latj13  14510  latj31  14511  latj4  14513  mod1ile  14517  mod2ile  14518  lubun  14533  latdisdlem  14598  lubunNEW  29502  oldmm1  29746  olj01  29754  latmassOLD  29758  omllaw5N  29776  cmtcomlemN  29777  cmtbr2N  29782  cmtbr3N  29783  cmtbr4N  29784  lecmtN  29785  omlfh1N  29787  omlfh3N  29788  omlmod1i2N  29789  cvlexchb1  29859  cvlcvr1  29868  hlatjcl  29895  exatleN  29932  cvrval3  29941  cvrexchlem  29947  cvrexch  29948  cvratlem  29949  cvrat  29950  lnnat  29955  cvrat2  29957  atcvrj2b  29960  atltcvr  29963  atlelt  29966  2atlt  29967  atexchcvrN  29968  cvrat3  29970  cvrat4  29971  2atjm  29973  4noncolr3  29981  athgt  29984  3dim0  29985  3dimlem4a  29991  1cvratex  30001  1cvrjat  30003  1cvrat  30004  ps-2  30006  3atlem1  30011  3atlem2  30012  3at  30018  2atm  30055  lplni2  30065  lplnle  30068  2llnmj  30088  2atmat  30089  lplnexllnN  30092  2llnjaN  30094  lvoli3  30105  islvol5  30107  lvoli2  30109  lvolnle3at  30110  3atnelvolN  30114  islvol2aN  30120  4atlem3  30124  4atlem4d  30130  4atlem9  30131  4atlem10a  30132  4atlem10  30134  4atlem11a  30135  4atlem11b  30136  4atlem11  30137  4atlem12a  30138  4atlem12b  30139  4atlem12  30140  4at  30141  lplncvrlvol2  30143  2lplnja  30147  2lplnmj  30150  dalem5  30195  dalem8  30198  dalem-cly  30199  dalem38  30238  dalem39  30239  dalem44  30244  dalem54  30254  linepsubN  30280  pmapsub  30296  isline2  30302  linepmap  30303  isline3  30304  lncvrelatN  30309  2llnma1b  30314  cdlema1N  30319  cdlemblem  30321  cdlemb  30322  paddasslem5  30352  paddasslem12  30359  paddasslem13  30360  pmapjoin  30380  pmapjat1  30381  pmapjlln1  30383  hlmod1i  30384  llnmod1i2  30388  atmod2i1  30389  atmod2i2  30390  llnmod2i2  30391  atmod3i1  30392  atmod3i2  30393  dalawlem2  30400  dalawlem3  30401  dalawlem5  30403  dalawlem6  30404  dalawlem7  30405  dalawlem8  30406  dalawlem11  30409  dalawlem12  30410  pmapocjN  30458  paddatclN  30477  linepsubclN  30479  pl42lem1N  30507  pl42lem2N  30508  pl42N  30511  lhp2lt  30529  lhpj1  30550  lhpmod2i2  30566  lhpmod6i1  30567  4atexlemc  30597  lautj  30621  trlval2  30691  trlcl  30692  trljat1  30694  trljat2  30695  trlle  30712  cdlemc1  30719  cdlemc2  30720  cdlemc5  30723  cdlemd2  30727  cdlemd3  30728  cdleme0aa  30738  cdleme0b  30740  cdleme0c  30741  cdleme0cp  30742  cdleme0cq  30743  cdleme0fN  30746  cdleme1b  30754  cdleme1  30755  cdleme2  30756  cdleme3b  30757  cdleme3c  30758  cdleme4a  30767  cdleme5  30768  cdleme7e  30775  cdleme8  30778  cdleme9  30781  cdleme10  30782  cdleme11fN  30792  cdleme11g  30793  cdleme11k  30796  cdleme11  30798  cdleme15b  30803  cdleme15  30806  cdleme22gb  30822  cdleme19b  30832  cdleme20d  30840  cdleme20j  30846  cdleme20l  30850  cdleme20m  30851  cdleme22e  30872  cdleme22eALTN  30873  cdleme22f  30874  cdleme23b  30878  cdleme23c  30879  cdleme28a  30898  cdleme28b  30899  cdleme29ex  30902  cdleme30a  30906  cdlemefr29exN  30930  cdleme32e  30973  cdleme35fnpq  30977  cdleme35b  30978  cdleme35c  30979  cdleme42e  31007  cdleme42i  31011  cdleme42mgN  31016  cdlemg2fv2  31128  cdlemg7fvbwN  31135  cdlemg4c  31140  cdlemg6c  31148  cdlemg10  31169  cdlemg11b  31170  cdlemg31a  31225  cdlemg31b  31226  cdlemg35  31241  trlcolem  31254  cdlemg44a  31259  trljco  31268  tendopltp  31308  cdlemh1  31343  cdlemh2  31344  cdlemi1  31346  cdlemi  31348  cdlemk4  31362  cdlemkvcl  31370  cdlemk10  31371  cdlemk11  31377  cdlemk11u  31399  cdlemk37  31442  cdlemkid1  31450  cdlemk50  31480  cdlemk51  31481  cdlemk52  31482  dialss  31575  dia2dimlem2  31594  dia2dimlem3  31595  cdlemm10N  31647  docaclN  31653  doca2N  31655  djajN  31666  diblss  31699  cdlemn2  31724  cdlemn10  31735  dihord1  31747  dihord2pre2  31755  dihord5apre  31791  dihjatc1  31840  dihmeetlem10N  31845  dihmeetlem11N  31846  djhljjN  31931  djhj  31933  dihprrnlem1N  31953  dihprrnlem2  31954  dihjat6  31963  dihjat5N  31966  dvh4dimat  31967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-iota 5404  df-fv 5448  df-ov 6070  df-lat 14458
  Copyright terms: Public domain W3C validator