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

Theorem latjcl 14471
Description: Closure of join operation in a lattice. (chjcom 23000 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 2435 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14469 . 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 5446  (class class class)co 6073   Basecbs 13461   joincjn 14393   meetcmee 14394   Latclat 14466
This theorem is referenced by:  latjcom  14480  latlej1  14481  latlej2  14482  latjle12  14483  latleeqj1  14484  latjlej1  14486  latjlej12  14488  latnlej2  14492  latjidm  14495  latnle  14506  latabs2  14509  latledi  14510  latmlej11  14511  latjass  14516  latj13  14519  latj31  14520  latj4  14522  mod1ile  14526  mod2ile  14527  lubun  14542  latdisdlem  14607  lubunNEW  29708  oldmm1  29952  olj01  29960  latmassOLD  29964  omllaw5N  29982  cmtcomlemN  29983  cmtbr2N  29988  cmtbr3N  29989  cmtbr4N  29990  lecmtN  29991  omlfh1N  29993  omlfh3N  29994  omlmod1i2N  29995  cvlexchb1  30065  cvlcvr1  30074  hlatjcl  30101  exatleN  30138  cvrval3  30147  cvrexchlem  30153  cvrexch  30154  cvratlem  30155  cvrat  30156  lnnat  30161  cvrat2  30163  atcvrj2b  30166  atltcvr  30169  atlelt  30172  2atlt  30173  atexchcvrN  30174  cvrat3  30176  cvrat4  30177  2atjm  30179  4noncolr3  30187  athgt  30190  3dim0  30191  3dimlem4a  30197  1cvratex  30207  1cvrjat  30209  1cvrat  30210  ps-2  30212  3atlem1  30217  3atlem2  30218  3at  30224  2atm  30261  lplni2  30271  lplnle  30274  2llnmj  30294  2atmat  30295  lplnexllnN  30298  2llnjaN  30300  lvoli3  30311  islvol5  30313  lvoli2  30315  lvolnle3at  30316  3atnelvolN  30320  islvol2aN  30326  4atlem3  30330  4atlem4d  30336  4atlem9  30337  4atlem10a  30338  4atlem10  30340  4atlem11a  30341  4atlem11b  30342  4atlem11  30343  4atlem12a  30344  4atlem12b  30345  4atlem12  30346  4at  30347  lplncvrlvol2  30349  2lplnja  30353  2lplnmj  30356  dalem5  30401  dalem8  30404  dalem-cly  30405  dalem38  30444  dalem39  30445  dalem44  30450  dalem54  30460  linepsubN  30486  pmapsub  30502  isline2  30508  linepmap  30509  isline3  30510  lncvrelatN  30515  2llnma1b  30520  cdlema1N  30525  cdlemblem  30527  cdlemb  30528  paddasslem5  30558  paddasslem12  30565  paddasslem13  30566  pmapjoin  30586  pmapjat1  30587  pmapjlln1  30589  hlmod1i  30590  llnmod1i2  30594  atmod2i1  30595  atmod2i2  30596  llnmod2i2  30597  atmod3i1  30598  atmod3i2  30599  dalawlem2  30606  dalawlem3  30607  dalawlem5  30609  dalawlem6  30610  dalawlem7  30611  dalawlem8  30612  dalawlem11  30615  dalawlem12  30616  pmapocjN  30664  paddatclN  30683  linepsubclN  30685  pl42lem1N  30713  pl42lem2N  30714  pl42N  30717  lhp2lt  30735  lhpj1  30756  lhpmod2i2  30772  lhpmod6i1  30773  4atexlemc  30803  lautj  30827  trlval2  30897  trlcl  30898  trljat1  30900  trljat2  30901  trlle  30918  cdlemc1  30925  cdlemc2  30926  cdlemc5  30929  cdlemd2  30933  cdlemd3  30934  cdleme0aa  30944  cdleme0b  30946  cdleme0c  30947  cdleme0cp  30948  cdleme0cq  30949  cdleme0fN  30952  cdleme1b  30960  cdleme1  30961  cdleme2  30962  cdleme3b  30963  cdleme3c  30964  cdleme4a  30973  cdleme5  30974  cdleme7e  30981  cdleme8  30984  cdleme9  30987  cdleme10  30988  cdleme11fN  30998  cdleme11g  30999  cdleme11k  31002  cdleme11  31004  cdleme15b  31009  cdleme15  31012  cdleme22gb  31028  cdleme19b  31038  cdleme20d  31046  cdleme20j  31052  cdleme20l  31056  cdleme20m  31057  cdleme22e  31078  cdleme22eALTN  31079  cdleme22f  31080  cdleme23b  31084  cdleme23c  31085  cdleme28a  31104  cdleme28b  31105  cdleme29ex  31108  cdleme30a  31112  cdlemefr29exN  31136  cdleme32e  31179  cdleme35fnpq  31183  cdleme35b  31184  cdleme35c  31185  cdleme42e  31213  cdleme42i  31217  cdleme42mgN  31222  cdlemg2fv2  31334  cdlemg7fvbwN  31341  cdlemg4c  31346  cdlemg6c  31354  cdlemg10  31375  cdlemg11b  31376  cdlemg31a  31431  cdlemg31b  31432  cdlemg35  31447  trlcolem  31460  cdlemg44a  31465  trljco  31474  tendopltp  31514  cdlemh1  31549  cdlemh2  31550  cdlemi1  31552  cdlemi  31554  cdlemk4  31568  cdlemkvcl  31576  cdlemk10  31577  cdlemk11  31583  cdlemk11u  31605  cdlemk37  31648  cdlemkid1  31656  cdlemk50  31686  cdlemk51  31687  cdlemk52  31688  dialss  31781  dia2dimlem2  31800  dia2dimlem3  31801  cdlemm10N  31853  docaclN  31859  doca2N  31861  djajN  31872  diblss  31905  cdlemn2  31930  cdlemn10  31941  dihord1  31953  dihord2pre2  31961  dihord5apre  31997  dihjatc1  32046  dihmeetlem10N  32051  dihmeetlem11N  32052  djhljjN  32137  djhj  32139  dihprrnlem1N  32159  dihprrnlem2  32160  dihjat6  32169  dihjat5N  32172  dvh4dimat  32173
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-lat 14467
  Copyright terms: Public domain W3C validator