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

Theorem latmcl 17274
Description: Closure of meet operation in a lattice. (incom 3949 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 2761 . . 3 (join‘𝐾) = (join‘𝐾)
3 latmcl.m . . 3 = (meet‘𝐾)
41, 2, 3latlem 17271 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 𝑌) ∈ 𝐵))
54simprd 482 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1632  wcel 2140  cfv 6050  (class class class)co 6815  Basecbs 16080  joincjn 17166  meetcmee 17167  Latclat 17267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-ov 6818  df-oprab 6819  df-lub 17196  df-glb 17197  df-join 17198  df-meet 17199  df-lat 17268
This theorem is referenced by:  latleeqm1  17301  latmlem1  17303  latmlem12  17305  latnlemlt  17306  latmidm  17308  latabs1  17309  latledi  17311  latmlej11  17312  mod1ile  17327  mod2ile  17328  latdisdlem  17411  oldmm1  35026  oldmj1  35030  latmrot  35041  latm4  35042  olm01  35045  omllaw4  35055  cmtcomlemN  35057  cmt2N  35059  cmtbr2N  35062  cmtbr3N  35063  cmtbr4N  35064  lecmtN  35065  omlfh1N  35067  omlfh3N  35068  meetat  35105  atnle  35126  atlatmstc  35128  hlrelat2  35211  cvrval5  35223  cvrexchlem  35227  cvrexch  35228  cvrat3  35250  cvrat4  35251  ps-2b  35290  2llnmat  35332  2atm  35335  llnmlplnN  35347  2lplnmN  35367  2llnmj  35368  2llnm2N  35376  2llnm4  35378  2lplnm2N  35429  2lplnmj  35430  dalemcea  35468  dalem16  35487  dalem21  35502  dalem54  35534  dalem55  35535  2lnat  35592  2atm2atN  35593  cdlema1N  35599  hlmod1i  35664  atmod1i1m  35666  atmod2i1  35669  atmod2i2  35670  llnmod2i2  35671  atmod4i1  35674  atmod4i2  35675  llnexchb2lem  35676  dalawlem1  35679  dalawlem2  35680  dalawlem3  35681  dalawlem4  35682  dalawlem5  35683  dalawlem6  35684  dalawlem7  35685  dalawlem8  35686  dalawlem9  35687  dalawlem11  35689  dalawlem12  35690  pmapj2N  35737  psubclinN  35756  poml4N  35761  pl42lem1N  35787  pl42lem2N  35788  pl42N  35791  lhpmcvr3  35833  lhpmcvr4N  35834  lhpmcvr5N  35835  lhpmcvr6N  35836  lhpelim  35845  lhpmod2i2  35846  lhpmod6i1  35847  lhprelat3N  35848  lautm  35902  trlval2  35972  trlcl  35973  trlval3  35996  cdlemc1  36000  cdlemc2  36001  cdlemc4  36003  cdlemc5  36004  cdlemc6  36005  cdlemd2  36008  cdleme0aa  36019  cdleme1b  36035  cdleme1  36036  cdleme2  36037  cdleme3b  36038  cdleme3h  36044  cdleme4a  36048  cdleme5  36049  cdleme7e  36056  cdleme7ga  36057  cdleme9b  36061  cdleme11g  36074  cdleme15d  36086  cdleme15  36087  cdleme16b  36088  cdleme16e  36091  cdleme16f  36092  cdleme22gb  36103  cdlemedb  36106  cdleme20j  36127  cdleme22cN  36151  cdleme22e  36153  cdleme22eALTN  36154  cdleme22f  36155  cdleme23a  36158  cdleme23b  36159  cdleme23c  36160  cdleme28a  36179  cdleme28b  36180  cdleme29ex  36183  cdleme30a  36187  cdlemefr29exN  36211  cdleme32c  36252  cdleme32e  36254  cdleme35b  36259  cdleme35c  36260  cdleme35d  36261  cdleme42c  36281  cdleme42h  36291  cdleme42i  36292  cdleme48bw  36311  cdlemg7fvbwN  36416  cdlemg10bALTN  36445  cdlemg10  36450  cdlemg11b  36451  cdlemg12f  36457  cdlemg12g  36458  cdlemg17a  36470  trlcolem  36535  cdlemkvcl  36651  cdlemk5u  36670  cdlemk37  36723  cdlemk52  36763  dia2dimlem2  36875  docaclN  36934  doca2N  36936  djajN  36947  cdlemn10  37016  dihjustlem  37026  dihord1  37028  dihord2a  37029  dihord2b  37030  dihord2cN  37031  dihord11b  37032  dihord11c  37034  dihord2pre  37035  dihord2pre2  37036  dihlsscpre  37044  dihvalcq2  37057  dihopelvalcpre  37058  dihord6apre  37066  dihord5b  37069  dihord5apre  37072  dihmeetlem1N  37100  dihglblem5apreN  37101  dihglblem2aN  37103  dihglblem2N  37104  dihmeetlem2N  37109  dihglbcpreN  37110  dihmeetbclemN  37114  dihmeetlem3N  37115  dihmeetlem4preN  37116  dihmeetlem6  37119  dihmeetlem7N  37120  dihjatc1  37121  dihjatc2N  37122  dihjatc3  37123  dihmeetlem9N  37125  dihmeetlem16N  37132  dihmeetlem19N  37135  dihmeetcl  37155  dihmeet2  37156  djhlj  37211  dihjatcclem1  37228  dihjatcclem2  37229  dihjatcclem4  37231
  Copyright terms: Public domain W3C validator