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

Theorem latmcl 17658
Description: Closure of meet operation in a lattice. (incom 4131 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 2801 . . 3 (join‘𝐾) = (join‘𝐾)
3 latmcl.m . . 3 = (meet‘𝐾)
41, 2, 3latlem 17655 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 𝑌) ∈ 𝐵))
54simprd 499 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2112  cfv 6328  (class class class)co 7139  Basecbs 16479  joincjn 17550  meetcmee 17551  Latclat 17651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-lub 17580  df-glb 17581  df-join 17582  df-meet 17583  df-lat 17652
This theorem is referenced by:  latleeqm1  17685  latmlem1  17687  latmlem12  17689  latnlemlt  17690  latmidm  17692  latabs1  17693  latledi  17695  latmlej11  17696  mod1ile  17711  mod2ile  17712  latdisdlem  17795  oldmm1  36512  oldmj1  36516  latmrot  36527  latm4  36528  olm01  36531  omllaw4  36541  cmtcomlemN  36543  cmt2N  36545  cmtbr2N  36548  cmtbr3N  36549  cmtbr4N  36550  lecmtN  36551  omlfh1N  36553  omlfh3N  36554  meetat  36591  atnle  36612  atlatmstc  36614  hlrelat2  36698  cvrval5  36710  cvrexchlem  36714  cvrexch  36715  cvrat3  36737  cvrat4  36738  ps-2b  36777  2llnmat  36819  2atm  36822  llnmlplnN  36834  2lplnmN  36854  2llnmj  36855  2llnm2N  36863  2llnm4  36865  2lplnm2N  36916  2lplnmj  36917  dalemcea  36955  dalem16  36974  dalem21  36989  dalem54  37021  dalem55  37022  2lnat  37079  2atm2atN  37080  cdlema1N  37086  hlmod1i  37151  atmod1i1m  37153  atmod2i1  37156  atmod2i2  37157  llnmod2i2  37158  atmod4i1  37161  atmod4i2  37162  llnexchb2lem  37163  dalawlem1  37166  dalawlem2  37167  dalawlem3  37168  dalawlem4  37169  dalawlem5  37170  dalawlem6  37171  dalawlem7  37172  dalawlem8  37173  dalawlem9  37174  dalawlem11  37176  dalawlem12  37177  pmapj2N  37224  psubclinN  37243  poml4N  37248  pl42lem1N  37274  pl42lem2N  37275  pl42N  37278  lhpmcvr3  37320  lhpmcvr4N  37321  lhpmcvr5N  37322  lhpmcvr6N  37323  lhpelim  37332  lhpmod2i2  37333  lhpmod6i1  37334  lhprelat3N  37335  lautm  37389  trlval2  37458  trlcl  37459  trlval3  37482  cdlemc1  37486  cdlemc2  37487  cdlemc4  37489  cdlemc5  37490  cdlemc6  37491  cdlemd2  37494  cdleme0aa  37505  cdleme1b  37521  cdleme1  37522  cdleme2  37523  cdleme3b  37524  cdleme3h  37530  cdleme4a  37534  cdleme5  37535  cdleme7e  37542  cdleme7ga  37543  cdleme9b  37547  cdleme11g  37560  cdleme15d  37572  cdleme15  37573  cdleme16b  37574  cdleme16e  37577  cdleme16f  37578  cdleme22gb  37589  cdlemedb  37592  cdleme20j  37613  cdleme22cN  37637  cdleme22e  37639  cdleme22eALTN  37640  cdleme22f  37641  cdleme23a  37644  cdleme23b  37645  cdleme23c  37646  cdleme28a  37665  cdleme28b  37666  cdleme29ex  37669  cdleme30a  37673  cdlemefr29exN  37697  cdleme32c  37738  cdleme32e  37740  cdleme35b  37745  cdleme35c  37746  cdleme35d  37747  cdleme42c  37767  cdleme42h  37777  cdleme42i  37778  cdleme48bw  37797  cdlemg7fvbwN  37902  cdlemg10bALTN  37931  cdlemg10  37936  cdlemg11b  37937  cdlemg12f  37943  cdlemg12g  37944  cdlemg17a  37956  trlcolem  38021  cdlemkvcl  38137  cdlemk5u  38156  cdlemk37  38209  cdlemk52  38249  dia2dimlem2  38360  docaclN  38419  doca2N  38421  djajN  38432  cdlemn10  38501  dihjustlem  38511  dihord1  38513  dihord2a  38514  dihord2b  38515  dihord2cN  38516  dihord11b  38517  dihord11c  38519  dihord2pre  38520  dihord2pre2  38521  dihlsscpre  38529  dihvalcq2  38542  dihopelvalcpre  38543  dihord6apre  38551  dihord5b  38554  dihord5apre  38557  dihmeetlem1N  38585  dihglblem5apreN  38586  dihglblem2aN  38588  dihglblem2N  38589  dihmeetlem2N  38594  dihglbcpreN  38595  dihmeetbclemN  38599  dihmeetlem3N  38600  dihmeetlem4preN  38601  dihmeetlem6  38604  dihmeetlem7N  38605  dihjatc1  38606  dihjatc2N  38607  dihjatc3  38608  dihmeetlem9N  38610  dihmeetlem16N  38617  dihmeetlem19N  38620  dihmeetcl  38640  dihmeet2  38641  djhlj  38696  dihjatcclem1  38713  dihjatcclem2  38714  dihjatcclem4  38716
  Copyright terms: Public domain W3C validator