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

Theorem latjcl 14172
Description: Closure of join operation in a lattice. (chjcom 22101 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 2296 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14170 . 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 1632    e. wcel 1696   ` cfv 5271  (class class class)co 5874   Basecbs 13164   joincjn 14094   meetcmee 14095   Latclat 14167
This theorem is referenced by:  latjcom  14181  latlej1  14182  latlej2  14183  latjle12  14184  latleeqj1  14185  latjlej1  14187  latjlej12  14189  latnlej2  14193  latjidm  14196  latnle  14207  latabs2  14210  latledi  14211  latmlej11  14212  latjass  14217  latj13  14220  latj31  14221  latj4  14223  mod1ile  14227  mod2ile  14228  lubun  14243  latdisdlem  14308  lubunNEW  29785  oldmm1  30029  olj01  30037  latmassOLD  30041  omllaw5N  30059  cmtcomlemN  30060  cmtbr2N  30065  cmtbr3N  30066  cmtbr4N  30067  lecmtN  30068  omlfh1N  30070  omlfh3N  30071  omlmod1i2N  30072  cvlexchb1  30142  cvlcvr1  30151  hlatjcl  30178  exatleN  30215  cvrval3  30224  cvrexchlem  30230  cvrexch  30231  cvratlem  30232  cvrat  30233  lnnat  30238  cvrat2  30240  atcvrj2b  30243  atltcvr  30246  atlelt  30249  2atlt  30250  atexchcvrN  30251  cvrat3  30253  cvrat4  30254  2atjm  30256  4noncolr3  30264  athgt  30267  3dim0  30268  3dimlem4a  30274  1cvratex  30284  1cvrjat  30286  1cvrat  30287  ps-2  30289  3atlem1  30294  3atlem2  30295  3at  30301  2atm  30338  lplni2  30348  lplnle  30351  2llnmj  30371  2atmat  30372  lplnexllnN  30375  2llnjaN  30377  lvoli3  30388  islvol5  30390  lvoli2  30392  lvolnle3at  30393  3atnelvolN  30397  islvol2aN  30403  4atlem3  30407  4atlem4d  30413  4atlem9  30414  4atlem10a  30415  4atlem10  30417  4atlem11a  30418  4atlem11b  30419  4atlem11  30420  4atlem12a  30421  4atlem12b  30422  4atlem12  30423  4at  30424  lplncvrlvol2  30426  2lplnja  30430  2lplnmj  30433  dalem5  30478  dalem8  30481  dalem-cly  30482  dalem38  30521  dalem39  30522  dalem44  30527  dalem54  30537  linepsubN  30563  pmapsub  30579  isline2  30585  linepmap  30586  isline3  30587  lncvrelatN  30592  2llnma1b  30597  cdlema1N  30602  cdlemblem  30604  cdlemb  30605  paddasslem5  30635  paddasslem12  30642  paddasslem13  30643  pmapjoin  30663  pmapjat1  30664  pmapjlln1  30666  hlmod1i  30667  llnmod1i2  30671  atmod2i1  30672  atmod2i2  30673  llnmod2i2  30674  atmod3i1  30675  atmod3i2  30676  dalawlem2  30683  dalawlem3  30684  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem11  30692  dalawlem12  30693  pmapocjN  30741  paddatclN  30760  linepsubclN  30762  pl42lem1N  30790  pl42lem2N  30791  pl42N  30794  lhp2lt  30812  lhpj1  30833  lhpmod2i2  30849  lhpmod6i1  30850  4atexlemc  30880  lautj  30904  trlval2  30974  trlcl  30975  trljat1  30977  trljat2  30978  trlle  30995  cdlemc1  31002  cdlemc2  31003  cdlemc5  31006  cdlemd2  31010  cdlemd3  31011  cdleme0aa  31021  cdleme0b  31023  cdleme0c  31024  cdleme0cp  31025  cdleme0cq  31026  cdleme0fN  31029  cdleme1b  31037  cdleme1  31038  cdleme2  31039  cdleme3b  31040  cdleme3c  31041  cdleme4a  31050  cdleme5  31051  cdleme7e  31058  cdleme8  31061  cdleme9  31064  cdleme10  31065  cdleme11fN  31075  cdleme11g  31076  cdleme11k  31079  cdleme11  31081  cdleme15b  31086  cdleme15  31089  cdleme22gb  31105  cdleme19b  31115  cdleme20d  31123  cdleme20j  31129  cdleme20l  31133  cdleme20m  31134  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme23b  31161  cdleme23c  31162  cdleme28a  31181  cdleme28b  31182  cdleme29ex  31185  cdleme30a  31189  cdlemefr29exN  31213  cdleme32e  31256  cdleme35fnpq  31260  cdleme35b  31261  cdleme35c  31262  cdleme42e  31290  cdleme42i  31294  cdleme42mgN  31299  cdlemg2fv2  31411  cdlemg7fvbwN  31418  cdlemg4c  31423  cdlemg6c  31431  cdlemg10  31452  cdlemg11b  31453  cdlemg31a  31508  cdlemg31b  31509  cdlemg35  31524  trlcolem  31537  cdlemg44a  31542  trljco  31551  tendopltp  31591  cdlemh1  31626  cdlemh2  31627  cdlemi1  31629  cdlemi  31631  cdlemk4  31645  cdlemkvcl  31653  cdlemk10  31654  cdlemk11  31660  cdlemk11u  31682  cdlemk37  31725  cdlemkid1  31733  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  dialss  31858  dia2dimlem2  31877  dia2dimlem3  31878  cdlemm10N  31930  docaclN  31936  doca2N  31938  djajN  31949  diblss  31982  cdlemn2  32007  cdlemn10  32018  dihord1  32030  dihord2pre2  32038  dihord5apre  32074  dihjatc1  32123  dihmeetlem10N  32128  dihmeetlem11N  32129  djhljjN  32214  djhj  32216  dihprrnlem1N  32236  dihprrnlem2  32237  dihjat6  32246  dihjat5N  32249  dvh4dimat  32250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-lat 14168
  Copyright terms: Public domain W3C validator