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

Theorem latmcl 16973
Description: Closure of meet operation in a lattice. (incom 3783 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 2621 . . 3 (join‘𝐾) = (join‘𝐾)
3 latmcl.m . . 3 = (meet‘𝐾)
41, 2, 3latlem 16970 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 𝑌) ∈ 𝐵))
54simprd 479 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1480  wcel 1987  cfv 5847  (class class class)co 6604  Basecbs 15781  joincjn 16865  meetcmee 16866  Latclat 16966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-lub 16895  df-glb 16896  df-join 16897  df-meet 16898  df-lat 16967
This theorem is referenced by:  latleeqm1  17000  latmlem1  17002  latmlem12  17004  latnlemlt  17005  latmidm  17007  latabs1  17008  latledi  17010  latmlej11  17011  mod1ile  17026  mod2ile  17027  latdisdlem  17110  oldmm1  33984  oldmj1  33988  latmrot  33999  latm4  34000  olm01  34003  omllaw4  34013  cmtcomlemN  34015  cmt2N  34017  cmtbr2N  34020  cmtbr3N  34021  cmtbr4N  34022  lecmtN  34023  omlfh1N  34025  omlfh3N  34026  meetat  34063  atnle  34084  atlatmstc  34086  hlrelat2  34169  cvrval5  34181  cvrexchlem  34185  cvrexch  34186  cvrat3  34208  cvrat4  34209  ps-2b  34248  2llnmat  34290  2atm  34293  llnmlplnN  34305  2lplnmN  34325  2llnmj  34326  2llnm2N  34334  2llnm4  34336  2lplnm2N  34387  2lplnmj  34388  dalemcea  34426  dalem16  34445  dalem21  34460  dalem54  34492  dalem55  34493  2lnat  34550  2atm2atN  34551  cdlema1N  34557  hlmod1i  34622  atmod1i1m  34624  atmod2i1  34627  atmod2i2  34628  llnmod2i2  34629  atmod4i1  34632  atmod4i2  34633  llnexchb2lem  34634  dalawlem1  34637  dalawlem2  34638  dalawlem3  34639  dalawlem4  34640  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem9  34645  dalawlem11  34647  dalawlem12  34648  pmapj2N  34695  psubclinN  34714  poml4N  34719  pl42lem1N  34745  pl42lem2N  34746  pl42N  34749  lhpmcvr3  34791  lhpmcvr4N  34792  lhpmcvr5N  34793  lhpmcvr6N  34794  lhpelim  34803  lhpmod2i2  34804  lhpmod6i1  34805  lhprelat3N  34806  lautm  34860  trlval2  34930  trlcl  34931  trlval3  34954  cdlemc1  34958  cdlemc2  34959  cdlemc4  34961  cdlemc5  34962  cdlemc6  34963  cdlemd2  34966  cdleme0aa  34977  cdleme1b  34993  cdleme1  34994  cdleme2  34995  cdleme3b  34996  cdleme3h  35002  cdleme4a  35006  cdleme5  35007  cdleme7e  35014  cdleme7ga  35015  cdleme9b  35019  cdleme11g  35032  cdleme15d  35044  cdleme15  35045  cdleme16b  35046  cdleme16e  35049  cdleme16f  35050  cdleme22gb  35061  cdlemedb  35064  cdleme20j  35086  cdleme22cN  35110  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f  35114  cdleme23a  35117  cdleme23b  35118  cdleme23c  35119  cdleme28a  35138  cdleme28b  35139  cdleme29ex  35142  cdleme30a  35146  cdlemefr29exN  35170  cdleme32c  35211  cdleme32e  35213  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme42c  35240  cdleme42h  35250  cdleme42i  35251  cdleme48bw  35270  cdlemg7fvbwN  35375  cdlemg10bALTN  35404  cdlemg10  35409  cdlemg11b  35410  cdlemg12f  35416  cdlemg12g  35417  cdlemg17a  35429  trlcolem  35494  cdlemkvcl  35610  cdlemk5u  35629  cdlemk37  35682  cdlemk52  35722  dia2dimlem2  35834  docaclN  35893  doca2N  35895  djajN  35906  cdlemn10  35975  dihjustlem  35985  dihord1  35987  dihord2a  35988  dihord2b  35989  dihord2cN  35990  dihord11b  35991  dihord11c  35993  dihord2pre  35994  dihord2pre2  35995  dihlsscpre  36003  dihvalcq2  36016  dihopelvalcpre  36017  dihord6apre  36025  dihord5b  36028  dihord5apre  36031  dihmeetlem1N  36059  dihglblem5apreN  36060  dihglblem2aN  36062  dihglblem2N  36063  dihmeetlem2N  36068  dihglbcpreN  36069  dihmeetbclemN  36073  dihmeetlem3N  36074  dihmeetlem4preN  36075  dihmeetlem6  36078  dihmeetlem7N  36079  dihjatc1  36080  dihjatc2N  36081  dihjatc3  36082  dihmeetlem9N  36084  dihmeetlem16N  36091  dihmeetlem19N  36094  dihmeetcl  36114  dihmeet2  36115  djhlj  36170  dihjatcclem1  36187  dihjatcclem2  36188  dihjatcclem4  36190
  Copyright terms: Public domain W3C validator