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

Theorem latmcl 16875
Description: Closure of meet operation in a lattice. (incom 3767 analog.) (Contributed by NM, 14-Sep-2011.)
Hypotheses
Ref Expression
latmcl.b 𝐵 = (Base‘𝐾)
latmcl.m = (meet‘𝐾)
Assertion
Ref Expression
latmcl ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)

Proof of Theorem latmcl
StepHypRef Expression
1 latmcl.b . . 3 𝐵 = (Base‘𝐾)
2 eqid 2610 . . 3 (join‘𝐾) = (join‘𝐾)
3 latmcl.m . . 3 = (meet‘𝐾)
41, 2, 3latlem 16872 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 𝑌) ∈ 𝐵))
54simprd 478 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031   = wceq 1475  wcel 1977  cfv 5804  (class class class)co 6549  Basecbs 15695  joincjn 16767  meetcmee 16768  Latclat 16868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-lub 16797  df-glb 16798  df-join 16799  df-meet 16800  df-lat 16869
This theorem is referenced by:  latleeqm1  16902  latmlem1  16904  latmlem12  16906  latnlemlt  16907  latmidm  16909  latabs1  16910  latledi  16912  latmlej11  16913  mod1ile  16928  mod2ile  16929  latdisdlem  17012  oldmm1  33522  oldmj1  33526  latmrot  33537  latm4  33538  olm01  33541  omllaw4  33551  cmtcomlemN  33553  cmt2N  33555  cmtbr2N  33558  cmtbr3N  33559  cmtbr4N  33560  lecmtN  33561  omlfh1N  33563  omlfh3N  33564  meetat  33601  atnle  33622  atlatmstc  33624  hlrelat2  33707  cvrval5  33719  cvrexchlem  33723  cvrexch  33724  cvrat3  33746  cvrat4  33747  ps-2b  33786  2llnmat  33828  2atm  33831  llnmlplnN  33843  2lplnmN  33863  2llnmj  33864  2llnm2N  33872  2llnm4  33874  2lplnm2N  33925  2lplnmj  33926  dalemcea  33964  dalem16  33983  dalem21  33998  dalem54  34030  dalem55  34031  2lnat  34088  2atm2atN  34089  cdlema1N  34095  hlmod1i  34160  atmod1i1m  34162  atmod2i1  34165  atmod2i2  34166  llnmod2i2  34167  atmod4i1  34170  atmod4i2  34171  llnexchb2lem  34172  dalawlem1  34175  dalawlem2  34176  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  pmapj2N  34233  psubclinN  34252  poml4N  34257  pl42lem1N  34283  pl42lem2N  34284  pl42N  34287  lhpmcvr3  34329  lhpmcvr4N  34330  lhpmcvr5N  34331  lhpmcvr6N  34332  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  lhprelat3N  34344  lautm  34398  trlval2  34468  trlcl  34469  trlval3  34492  cdlemc1  34496  cdlemc2  34497  cdlemc4  34499  cdlemc5  34500  cdlemc6  34501  cdlemd2  34504  cdleme0aa  34515  cdleme1b  34531  cdleme1  34532  cdleme2  34533  cdleme3b  34534  cdleme3h  34540  cdleme4a  34544  cdleme5  34545  cdleme7e  34552  cdleme7ga  34553  cdleme9b  34557  cdleme11g  34570  cdleme15d  34582  cdleme15  34583  cdleme16b  34584  cdleme16e  34587  cdleme16f  34588  cdleme22gb  34599  cdlemedb  34602  cdleme20j  34624  cdleme22cN  34648  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme23a  34655  cdleme23b  34656  cdleme23c  34657  cdleme28a  34676  cdleme28b  34677  cdleme29ex  34680  cdleme30a  34684  cdlemefr29exN  34708  cdleme32c  34749  cdleme32e  34751  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme42c  34778  cdleme42h  34788  cdleme42i  34789  cdleme48bw  34808  cdlemg7fvbwN  34913  cdlemg10bALTN  34942  cdlemg10  34947  cdlemg11b  34948  cdlemg12f  34954  cdlemg12g  34955  cdlemg17a  34967  trlcolem  35032  cdlemkvcl  35148  cdlemk5u  35167  cdlemk37  35220  cdlemk52  35260  dia2dimlem2  35372  docaclN  35431  doca2N  35433  djajN  35444  cdlemn10  35513  dihjustlem  35523  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord2cN  35528  dihord11b  35529  dihord11c  35531  dihord2pre  35532  dihord2pre2  35533  dihlsscpre  35541  dihvalcq2  35554  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihord5apre  35569  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem2aN  35600  dihglblem2N  35601  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetbclemN  35611  dihmeetlem3N  35612  dihmeetlem4preN  35613  dihmeetlem6  35616  dihmeetlem7N  35617  dihjatc1  35618  dihjatc2N  35619  dihjatc3  35620  dihmeetlem9N  35622  dihmeetlem16N  35629  dihmeetlem19N  35632  dihmeetcl  35652  dihmeet2  35653  djhlj  35708  dihjatcclem1  35725  dihjatcclem2  35726  dihjatcclem4  35728
  Copyright terms: Public domain W3C validator