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

Theorem latmcl 14206
Description: Closure of meet operation in a lattice. (incom 3395 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 2316 . . 3  |-  ( join `  K )  =  (
join `  K )
3 latmcl.m . . 3  |-  ./\  =  ( meet `  K )
41, 2, 3latlem 14203 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X (
join `  K ) Y )  e.  B  /\  ( X  ./\  Y
)  e.  B ) )
54simprd 449 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 934    = wceq 1633    e. wcel 1701   ` cfv 5292  (class class class)co 5900   Basecbs 13195   joincjn 14127   meetcmee 14128   Latclat 14200
This theorem is referenced by:  latmcom  14230  latmle1  14231  latmle2  14232  latlem12  14233  latleeqm1  14234  latmlem1  14236  latmlem12  14238  latnlemlt  14239  latmidm  14241  latabs1  14242  latledi  14244  latmlej11  14245  mod1ile  14260  mod2ile  14261  latdisdlem  14341  oldmm1  29225  oldmj1  29229  latmrot  29240  latm4  29241  olm01  29244  omllaw4  29254  cmtcomlemN  29256  cmt2N  29258  cmtbr2N  29261  cmtbr3N  29262  cmtbr4N  29263  lecmtN  29264  omlfh1N  29266  omlfh3N  29267  meetat  29304  atnle  29325  atlatmstc  29327  hlrelat2  29410  cvrval5  29422  cvrexchlem  29426  cvrexch  29427  cvrat3  29449  cvrat4  29450  ps-2b  29489  2llnmat  29531  2atm  29534  llnmlplnN  29546  2lplnmN  29566  2llnmj  29567  2llnm2N  29575  2llnm4  29577  2lplnm2N  29628  2lplnmj  29629  dalemcea  29667  dalem16  29686  dalem21  29701  dalem54  29733  dalem55  29734  2lnat  29791  2atm2atN  29792  cdlema1N  29798  hlmod1i  29863  atmod1i1m  29865  atmod2i1  29868  atmod2i2  29869  llnmod2i2  29870  atmod4i1  29873  atmod4i2  29874  llnexchb2lem  29875  dalawlem1  29878  dalawlem2  29879  dalawlem3  29880  dalawlem4  29881  dalawlem5  29882  dalawlem6  29883  dalawlem7  29884  dalawlem8  29885  dalawlem9  29886  dalawlem11  29888  dalawlem12  29889  pmapj2N  29936  psubclinN  29955  poml4N  29960  pl42lem1N  29986  pl42lem2N  29987  pl42N  29990  lhpmcvr3  30032  lhpmcvr4N  30033  lhpmcvr5N  30034  lhpmcvr6N  30035  lhpelim  30044  lhpmod2i2  30045  lhpmod6i1  30046  lhprelat3N  30047  lautm  30101  trlval2  30170  trlcl  30171  trlval3  30194  cdlemc1  30198  cdlemc2  30199  cdlemc4  30201  cdlemc5  30202  cdlemc6  30203  cdlemd2  30206  cdleme0aa  30217  cdleme1b  30233  cdleme1  30234  cdleme2  30235  cdleme3b  30236  cdleme3h  30242  cdleme4a  30246  cdleme5  30247  cdleme7e  30254  cdleme7ga  30255  cdleme9b  30259  cdleme11g  30272  cdleme15d  30284  cdleme15  30285  cdleme16b  30286  cdleme16e  30289  cdleme16f  30290  cdleme22gb  30301  cdlemedb  30304  cdleme20j  30325  cdleme22cN  30349  cdleme22e  30351  cdleme22eALTN  30352  cdleme22f  30353  cdleme23a  30356  cdleme23b  30357  cdleme23c  30358  cdleme28a  30377  cdleme28b  30378  cdleme29ex  30381  cdleme30a  30385  cdlemefr29exN  30409  cdleme32c  30450  cdleme32e  30452  cdleme35b  30457  cdleme35c  30458  cdleme35d  30459  cdleme42c  30479  cdleme42h  30489  cdleme42i  30490  cdleme48bw  30509  cdlemg7fvbwN  30614  cdlemg10bALTN  30643  cdlemg10  30648  cdlemg11b  30649  cdlemg12f  30655  cdlemg12g  30656  cdlemg17a  30668  trlcolem  30733  cdlemkvcl  30849  cdlemk5u  30868  cdlemk37  30921  cdlemk52  30961  dia2dimlem2  31073  docaclN  31132  doca2N  31134  djajN  31145  cdlemn10  31214  dihjustlem  31224  dihord1  31226  dihord2a  31227  dihord2b  31228  dihord2cN  31229  dihord11b  31230  dihord11c  31232  dihord2pre  31233  dihord2pre2  31234  dihlsscpre  31242  dihvalcq2  31255  dihopelvalcpre  31256  dihord6apre  31264  dihord5b  31267  dihord5apre  31270  dihmeetlem1N  31298  dihglblem5apreN  31299  dihglblem2aN  31301  dihglblem2N  31302  dihmeetlem2N  31307  dihglbcpreN  31308  dihmeetbclemN  31312  dihmeetlem3N  31313  dihmeetlem4preN  31314  dihmeetlem6  31317  dihmeetlem7N  31318  dihjatc1  31319  dihjatc2N  31320  dihjatc3  31321  dihmeetlem9N  31323  dihmeetlem16N  31330  dihmeetlem19N  31333  dihmeetcl  31353  dihmeet2  31354  djhlj  31409  dihjatcclem1  31426  dihjatcclem2  31427  dihjatcclem4  31429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-lat 14201
  Copyright terms: Public domain W3C validator