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

Theorem latmcl 14472
Description: Closure of meet operation in a lattice. (incom 3525 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 2435 . . 3  |-  ( join `  K )  =  (
join `  K )
3 latmcl.m . . 3  |-  ./\  =  ( meet `  K )
41, 2, 3latlem 14469 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X (
join `  K ) Y )  e.  B  /\  ( X  ./\  Y
)  e.  B ) )
54simprd 450 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 936    = wceq 1652    e. wcel 1725   ` cfv 5446  (class class class)co 6073   Basecbs 13461   joincjn 14393   meetcmee 14394   Latclat 14466
This theorem is referenced by:  latmcom  14496  latmle1  14497  latmle2  14498  latlem12  14499  latleeqm1  14500  latmlem1  14502  latmlem12  14504  latnlemlt  14505  latmidm  14507  latabs1  14508  latledi  14510  latmlej11  14511  mod1ile  14526  mod2ile  14527  latdisdlem  14607  oldmm1  29952  oldmj1  29956  latmrot  29967  latm4  29968  olm01  29971  omllaw4  29981  cmtcomlemN  29983  cmt2N  29985  cmtbr2N  29988  cmtbr3N  29989  cmtbr4N  29990  lecmtN  29991  omlfh1N  29993  omlfh3N  29994  meetat  30031  atnle  30052  atlatmstc  30054  hlrelat2  30137  cvrval5  30149  cvrexchlem  30153  cvrexch  30154  cvrat3  30176  cvrat4  30177  ps-2b  30216  2llnmat  30258  2atm  30261  llnmlplnN  30273  2lplnmN  30293  2llnmj  30294  2llnm2N  30302  2llnm4  30304  2lplnm2N  30355  2lplnmj  30356  dalemcea  30394  dalem16  30413  dalem21  30428  dalem54  30460  dalem55  30461  2lnat  30518  2atm2atN  30519  cdlema1N  30525  hlmod1i  30590  atmod1i1m  30592  atmod2i1  30595  atmod2i2  30596  llnmod2i2  30597  atmod4i1  30600  atmod4i2  30601  llnexchb2lem  30602  dalawlem1  30605  dalawlem2  30606  dalawlem3  30607  dalawlem4  30608  dalawlem5  30609  dalawlem6  30610  dalawlem7  30611  dalawlem8  30612  dalawlem9  30613  dalawlem11  30615  dalawlem12  30616  pmapj2N  30663  psubclinN  30682  poml4N  30687  pl42lem1N  30713  pl42lem2N  30714  pl42N  30717  lhpmcvr3  30759  lhpmcvr4N  30760  lhpmcvr5N  30761  lhpmcvr6N  30762  lhpelim  30771  lhpmod2i2  30772  lhpmod6i1  30773  lhprelat3N  30774  lautm  30828  trlval2  30897  trlcl  30898  trlval3  30921  cdlemc1  30925  cdlemc2  30926  cdlemc4  30928  cdlemc5  30929  cdlemc6  30930  cdlemd2  30933  cdleme0aa  30944  cdleme1b  30960  cdleme1  30961  cdleme2  30962  cdleme3b  30963  cdleme3h  30969  cdleme4a  30973  cdleme5  30974  cdleme7e  30981  cdleme7ga  30982  cdleme9b  30986  cdleme11g  30999  cdleme15d  31011  cdleme15  31012  cdleme16b  31013  cdleme16e  31016  cdleme16f  31017  cdleme22gb  31028  cdlemedb  31031  cdleme20j  31052  cdleme22cN  31076  cdleme22e  31078  cdleme22eALTN  31079  cdleme22f  31080  cdleme23a  31083  cdleme23b  31084  cdleme23c  31085  cdleme28a  31104  cdleme28b  31105  cdleme29ex  31108  cdleme30a  31112  cdlemefr29exN  31136  cdleme32c  31177  cdleme32e  31179  cdleme35b  31184  cdleme35c  31185  cdleme35d  31186  cdleme42c  31206  cdleme42h  31216  cdleme42i  31217  cdleme48bw  31236  cdlemg7fvbwN  31341  cdlemg10bALTN  31370  cdlemg10  31375  cdlemg11b  31376  cdlemg12f  31382  cdlemg12g  31383  cdlemg17a  31395  trlcolem  31460  cdlemkvcl  31576  cdlemk5u  31595  cdlemk37  31648  cdlemk52  31688  dia2dimlem2  31800  docaclN  31859  doca2N  31861  djajN  31872  cdlemn10  31941  dihjustlem  31951  dihord1  31953  dihord2a  31954  dihord2b  31955  dihord2cN  31956  dihord11b  31957  dihord11c  31959  dihord2pre  31960  dihord2pre2  31961  dihlsscpre  31969  dihvalcq2  31982  dihopelvalcpre  31983  dihord6apre  31991  dihord5b  31994  dihord5apre  31997  dihmeetlem1N  32025  dihglblem5apreN  32026  dihglblem2aN  32028  dihglblem2N  32029  dihmeetlem2N  32034  dihglbcpreN  32035  dihmeetbclemN  32039  dihmeetlem3N  32040  dihmeetlem4preN  32041  dihmeetlem6  32044  dihmeetlem7N  32045  dihjatc1  32046  dihjatc2N  32047  dihjatc3  32048  dihmeetlem9N  32050  dihmeetlem16N  32057  dihmeetlem19N  32060  dihmeetcl  32080  dihmeet2  32081  djhlj  32136  dihjatcclem1  32153  dihjatcclem2  32154  dihjatcclem4  32156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-lat 14467
  Copyright terms: Public domain W3C validator