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

Theorem latjcl 14434
Description: Closure of join operation in a lattice. (chjcom 22961 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 2404 . . 3  |-  ( meet `  K )  =  (
meet `  K )
41, 2, 3latlem 14432 . 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 1721   ` cfv 5413  (class class class)co 6040   Basecbs 13424   joincjn 14356   meetcmee 14357   Latclat 14429
This theorem is referenced by:  latjcom  14443  latlej1  14444  latlej2  14445  latjle12  14446  latleeqj1  14447  latjlej1  14449  latjlej12  14451  latnlej2  14455  latjidm  14458  latnle  14469  latabs2  14472  latledi  14473  latmlej11  14474  latjass  14479  latj13  14482  latj31  14483  latj4  14485  mod1ile  14489  mod2ile  14490  lubun  14505  latdisdlem  14570  lubunNEW  29456  oldmm1  29700  olj01  29708  latmassOLD  29712  omllaw5N  29730  cmtcomlemN  29731  cmtbr2N  29736  cmtbr3N  29737  cmtbr4N  29738  lecmtN  29739  omlfh1N  29741  omlfh3N  29742  omlmod1i2N  29743  cvlexchb1  29813  cvlcvr1  29822  hlatjcl  29849  exatleN  29886  cvrval3  29895  cvrexchlem  29901  cvrexch  29902  cvratlem  29903  cvrat  29904  lnnat  29909  cvrat2  29911  atcvrj2b  29914  atltcvr  29917  atlelt  29920  2atlt  29921  atexchcvrN  29922  cvrat3  29924  cvrat4  29925  2atjm  29927  4noncolr3  29935  athgt  29938  3dim0  29939  3dimlem4a  29945  1cvratex  29955  1cvrjat  29957  1cvrat  29958  ps-2  29960  3atlem1  29965  3atlem2  29966  3at  29972  2atm  30009  lplni2  30019  lplnle  30022  2llnmj  30042  2atmat  30043  lplnexllnN  30046  2llnjaN  30048  lvoli3  30059  islvol5  30061  lvoli2  30063  lvolnle3at  30064  3atnelvolN  30068  islvol2aN  30074  4atlem3  30078  4atlem4d  30084  4atlem9  30085  4atlem10a  30086  4atlem10  30088  4atlem11a  30089  4atlem11b  30090  4atlem11  30091  4atlem12a  30092  4atlem12b  30093  4atlem12  30094  4at  30095  lplncvrlvol2  30097  2lplnja  30101  2lplnmj  30104  dalem5  30149  dalem8  30152  dalem-cly  30153  dalem38  30192  dalem39  30193  dalem44  30198  dalem54  30208  linepsubN  30234  pmapsub  30250  isline2  30256  linepmap  30257  isline3  30258  lncvrelatN  30263  2llnma1b  30268  cdlema1N  30273  cdlemblem  30275  cdlemb  30276  paddasslem5  30306  paddasslem12  30313  paddasslem13  30314  pmapjoin  30334  pmapjat1  30335  pmapjlln1  30337  hlmod1i  30338  llnmod1i2  30342  atmod2i1  30343  atmod2i2  30344  llnmod2i2  30345  atmod3i1  30346  atmod3i2  30347  dalawlem2  30354  dalawlem3  30355  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem11  30363  dalawlem12  30364  pmapocjN  30412  paddatclN  30431  linepsubclN  30433  pl42lem1N  30461  pl42lem2N  30462  pl42N  30465  lhp2lt  30483  lhpj1  30504  lhpmod2i2  30520  lhpmod6i1  30521  4atexlemc  30551  lautj  30575  trlval2  30645  trlcl  30646  trljat1  30648  trljat2  30649  trlle  30666  cdlemc1  30673  cdlemc2  30674  cdlemc5  30677  cdlemd2  30681  cdlemd3  30682  cdleme0aa  30692  cdleme0b  30694  cdleme0c  30695  cdleme0cp  30696  cdleme0cq  30697  cdleme0fN  30700  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3b  30711  cdleme3c  30712  cdleme4a  30721  cdleme5  30722  cdleme7e  30729  cdleme8  30732  cdleme9  30735  cdleme10  30736  cdleme11fN  30746  cdleme11g  30747  cdleme11k  30750  cdleme11  30752  cdleme15b  30757  cdleme15  30760  cdleme22gb  30776  cdleme19b  30786  cdleme20d  30794  cdleme20j  30800  cdleme20l  30804  cdleme20m  30805  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f  30828  cdleme23b  30832  cdleme23c  30833  cdleme28a  30852  cdleme28b  30853  cdleme29ex  30856  cdleme30a  30860  cdlemefr29exN  30884  cdleme32e  30927  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme42e  30961  cdleme42i  30965  cdleme42mgN  30970  cdlemg2fv2  31082  cdlemg7fvbwN  31089  cdlemg4c  31094  cdlemg6c  31102  cdlemg10  31123  cdlemg11b  31124  cdlemg31a  31179  cdlemg31b  31180  cdlemg35  31195  trlcolem  31208  cdlemg44a  31213  trljco  31222  tendopltp  31262  cdlemh1  31297  cdlemh2  31298  cdlemi1  31300  cdlemi  31302  cdlemk4  31316  cdlemkvcl  31324  cdlemk10  31325  cdlemk11  31331  cdlemk11u  31353  cdlemk37  31396  cdlemkid1  31404  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  dialss  31529  dia2dimlem2  31548  dia2dimlem3  31549  cdlemm10N  31601  docaclN  31607  doca2N  31609  djajN  31620  diblss  31653  cdlemn2  31678  cdlemn10  31689  dihord1  31701  dihord2pre2  31709  dihord5apre  31745  dihjatc1  31794  dihmeetlem10N  31799  dihmeetlem11N  31800  djhljjN  31885  djhj  31887  dihprrnlem1N  31907  dihprrnlem2  31908  dihjat6  31917  dihjat5N  31920  dvh4dimat  31921
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-lat 14430
  Copyright terms: Public domain W3C validator