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

Theorem latmcl 14157
Description: Closure of meet operation in a lattice. (incom 3361 analog.) (Contributed by NM, 14-Sep-2011.)
Hypotheses
Ref Expression
latmcl.b  |-  B  =  ( Base `  K
)
latmcl.m  |-  ./\  =  ( meet `  K )
Assertion
Ref Expression
latmcl  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  e.  B )

Proof of Theorem latmcl
StepHypRef Expression
1 latmcl.b . . 3  |-  B  =  ( Base `  K
)
2 eqid 2283 . . 3  |-  ( join `  K )  =  (
join `  K )
3 latmcl.m . . 3  |-  ./\  =  ( meet `  K )
41, 2, 3latlem 14154 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X (
join `  K ) Y )  e.  B  /\  ( X  ./\  Y
)  e.  B ) )
54simprd 449 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 1623    e. wcel 1684   ` cfv 5255  (class class class)co 5858   Basecbs 13148   joincjn 14078   meetcmee 14079   Latclat 14151
This theorem is referenced by:  latmcom  14181  latmle1  14182  latmle2  14183  latlem12  14184  latleeqm1  14185  latmlem1  14187  latmlem12  14189  latnlemlt  14190  latmidm  14192  latabs1  14193  latledi  14195  latmlej11  14196  mod1ile  14211  mod2ile  14212  latdisdlem  14292  oldmm1  29407  oldmj1  29411  latmrot  29422  latm4  29423  olm01  29426  omllaw4  29436  cmtcomlemN  29438  cmt2N  29440  cmtbr2N  29443  cmtbr3N  29444  cmtbr4N  29445  lecmtN  29446  omlfh1N  29448  omlfh3N  29449  meetat  29486  atnle  29507  atlatmstc  29509  hlrelat2  29592  cvrval5  29604  cvrexchlem  29608  cvrexch  29609  cvrat3  29631  cvrat4  29632  ps-2b  29671  2llnmat  29713  2atm  29716  llnmlplnN  29728  2lplnmN  29748  2llnmj  29749  2llnm2N  29757  2llnm4  29759  2lplnm2N  29810  2lplnmj  29811  dalemcea  29849  dalem16  29868  dalem21  29883  dalem54  29915  dalem55  29916  2lnat  29973  2atm2atN  29974  cdlema1N  29980  hlmod1i  30045  atmod1i1m  30047  atmod2i1  30050  atmod2i2  30051  llnmod2i2  30052  atmod4i1  30055  atmod4i2  30056  llnexchb2lem  30057  dalawlem1  30060  dalawlem2  30061  dalawlem3  30062  dalawlem4  30063  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem8  30067  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  pmapj2N  30118  psubclinN  30137  poml4N  30142  pl42lem1N  30168  pl42lem2N  30169  pl42N  30172  lhpmcvr3  30214  lhpmcvr4N  30215  lhpmcvr5N  30216  lhpmcvr6N  30217  lhpelim  30226  lhpmod2i2  30227  lhpmod6i1  30228  lhprelat3N  30229  lautm  30283  trlval2  30352  trlcl  30353  trlval3  30376  cdlemc1  30380  cdlemc2  30381  cdlemc4  30383  cdlemc5  30384  cdlemc6  30385  cdlemd2  30388  cdleme0aa  30399  cdleme1b  30415  cdleme1  30416  cdleme2  30417  cdleme3b  30418  cdleme3h  30424  cdleme4a  30428  cdleme5  30429  cdleme7e  30436  cdleme7ga  30437  cdleme9b  30441  cdleme11g  30454  cdleme15d  30466  cdleme15  30467  cdleme16b  30468  cdleme16e  30471  cdleme16f  30472  cdleme22gb  30483  cdlemedb  30486  cdleme20j  30507  cdleme22cN  30531  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme23a  30538  cdleme23b  30539  cdleme23c  30540  cdleme28a  30559  cdleme28b  30560  cdleme29ex  30563  cdleme30a  30567  cdlemefr29exN  30591  cdleme32c  30632  cdleme32e  30634  cdleme35b  30639  cdleme35c  30640  cdleme35d  30641  cdleme42c  30661  cdleme42h  30671  cdleme42i  30672  cdleme48bw  30691  cdlemg7fvbwN  30796  cdlemg10bALTN  30825  cdlemg10  30830  cdlemg11b  30831  cdlemg12f  30837  cdlemg12g  30838  cdlemg17a  30850  trlcolem  30915  cdlemkvcl  31031  cdlemk5u  31050  cdlemk37  31103  cdlemk52  31143  dia2dimlem2  31255  docaclN  31314  doca2N  31316  djajN  31327  cdlemn10  31396  dihjustlem  31406  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord2cN  31411  dihord11b  31412  dihord11c  31414  dihord2pre  31415  dihord2pre2  31416  dihlsscpre  31424  dihvalcq2  31437  dihopelvalcpre  31438  dihord6apre  31446  dihord5b  31449  dihord5apre  31452  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem2aN  31483  dihglblem2N  31484  dihmeetlem2N  31489  dihglbcpreN  31490  dihmeetbclemN  31494  dihmeetlem3N  31495  dihmeetlem4preN  31496  dihmeetlem6  31499  dihmeetlem7N  31500  dihjatc1  31501  dihjatc2N  31502  dihjatc3  31503  dihmeetlem9N  31505  dihmeetlem16N  31512  dihmeetlem19N  31515  dihmeetcl  31535  dihmeet2  31536  djhlj  31591  dihjatcclem1  31608  dihjatcclem2  31609  dihjatcclem4  31611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-lat 14152
  Copyright terms: Public domain W3C validator