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

Theorem latmcl 14485
Description: Closure of meet operation in a lattice. (incom 3535 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 2438 . . 3  |-  ( join `  K )  =  (
join `  K )
3 latmcl.m . . 3  |-  ./\  =  ( meet `  K )
41, 2, 3latlem 14482 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X (
join `  K ) Y )  e.  B  /\  ( X  ./\  Y
)  e.  B ) )
54simprd 451 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 937    = wceq 1653    e. wcel 1726   ` cfv 5457  (class class class)co 6084   Basecbs 13474   joincjn 14406   meetcmee 14407   Latclat 14479
This theorem is referenced by:  latmcom  14509  latmle1  14510  latmle2  14511  latlem12  14512  latleeqm1  14513  latmlem1  14515  latmlem12  14517  latnlemlt  14518  latmidm  14520  latabs1  14521  latledi  14523  latmlej11  14524  mod1ile  14539  mod2ile  14540  latdisdlem  14620  oldmm1  30088  oldmj1  30092  latmrot  30103  latm4  30104  olm01  30107  omllaw4  30117  cmtcomlemN  30119  cmt2N  30121  cmtbr2N  30124  cmtbr3N  30125  cmtbr4N  30126  lecmtN  30127  omlfh1N  30129  omlfh3N  30130  meetat  30167  atnle  30188  atlatmstc  30190  hlrelat2  30273  cvrval5  30285  cvrexchlem  30289  cvrexch  30290  cvrat3  30312  cvrat4  30313  ps-2b  30352  2llnmat  30394  2atm  30397  llnmlplnN  30409  2lplnmN  30429  2llnmj  30430  2llnm2N  30438  2llnm4  30440  2lplnm2N  30491  2lplnmj  30492  dalemcea  30530  dalem16  30549  dalem21  30564  dalem54  30596  dalem55  30597  2lnat  30654  2atm2atN  30655  cdlema1N  30661  hlmod1i  30726  atmod1i1m  30728  atmod2i1  30731  atmod2i2  30732  llnmod2i2  30733  atmod4i1  30736  atmod4i2  30737  llnexchb2lem  30738  dalawlem1  30741  dalawlem2  30742  dalawlem3  30743  dalawlem4  30744  dalawlem5  30745  dalawlem6  30746  dalawlem7  30747  dalawlem8  30748  dalawlem9  30749  dalawlem11  30751  dalawlem12  30752  pmapj2N  30799  psubclinN  30818  poml4N  30823  pl42lem1N  30849  pl42lem2N  30850  pl42N  30853  lhpmcvr3  30895  lhpmcvr4N  30896  lhpmcvr5N  30897  lhpmcvr6N  30898  lhpelim  30907  lhpmod2i2  30908  lhpmod6i1  30909  lhprelat3N  30910  lautm  30964  trlval2  31033  trlcl  31034  trlval3  31057  cdlemc1  31061  cdlemc2  31062  cdlemc4  31064  cdlemc5  31065  cdlemc6  31066  cdlemd2  31069  cdleme0aa  31080  cdleme1b  31096  cdleme1  31097  cdleme2  31098  cdleme3b  31099  cdleme3h  31105  cdleme4a  31109  cdleme5  31110  cdleme7e  31117  cdleme7ga  31118  cdleme9b  31122  cdleme11g  31135  cdleme15d  31147  cdleme15  31148  cdleme16b  31149  cdleme16e  31152  cdleme16f  31153  cdleme22gb  31164  cdlemedb  31167  cdleme20j  31188  cdleme22cN  31212  cdleme22e  31214  cdleme22eALTN  31215  cdleme22f  31216  cdleme23a  31219  cdleme23b  31220  cdleme23c  31221  cdleme28a  31240  cdleme28b  31241  cdleme29ex  31244  cdleme30a  31248  cdlemefr29exN  31272  cdleme32c  31313  cdleme32e  31315  cdleme35b  31320  cdleme35c  31321  cdleme35d  31322  cdleme42c  31342  cdleme42h  31352  cdleme42i  31353  cdleme48bw  31372  cdlemg7fvbwN  31477  cdlemg10bALTN  31506  cdlemg10  31511  cdlemg11b  31512  cdlemg12f  31518  cdlemg12g  31519  cdlemg17a  31531  trlcolem  31596  cdlemkvcl  31712  cdlemk5u  31731  cdlemk37  31784  cdlemk52  31824  dia2dimlem2  31936  docaclN  31995  doca2N  31997  djajN  32008  cdlemn10  32077  dihjustlem  32087  dihord1  32089  dihord2a  32090  dihord2b  32091  dihord2cN  32092  dihord11b  32093  dihord11c  32095  dihord2pre  32096  dihord2pre2  32097  dihlsscpre  32105  dihvalcq2  32118  dihopelvalcpre  32119  dihord6apre  32127  dihord5b  32130  dihord5apre  32133  dihmeetlem1N  32161  dihglblem5apreN  32162  dihglblem2aN  32164  dihglblem2N  32165  dihmeetlem2N  32170  dihglbcpreN  32171  dihmeetbclemN  32175  dihmeetlem3N  32176  dihmeetlem4preN  32177  dihmeetlem6  32180  dihmeetlem7N  32181  dihjatc1  32182  dihjatc2N  32183  dihjatc3  32184  dihmeetlem9N  32186  dihmeetlem16N  32193  dihmeetlem19N  32196  dihmeetcl  32216  dihmeet2  32217  djhlj  32272  dihjatcclem1  32289  dihjatcclem2  32290  dihjatcclem4  32292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-lat 14480
  Copyright terms: Public domain W3C validator