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

Theorem latmcl 14173
Description: Closure of meet operation in a lattice. (incom 3374 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 2296 . . 3  |-  ( join `  K )  =  (
join `  K )
3 latmcl.m . . 3  |-  ./\  =  ( meet `  K )
41, 2, 3latlem 14170 . 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 1632    e. wcel 1696   ` cfv 5271  (class class class)co 5874   Basecbs 13164   joincjn 14094   meetcmee 14095   Latclat 14167
This theorem is referenced by:  latmcom  14197  latmle1  14198  latmle2  14199  latlem12  14200  latleeqm1  14201  latmlem1  14203  latmlem12  14205  latnlemlt  14206  latmidm  14208  latabs1  14209  latledi  14211  latmlej11  14212  mod1ile  14227  mod2ile  14228  latdisdlem  14308  oldmm1  30029  oldmj1  30033  latmrot  30044  latm4  30045  olm01  30048  omllaw4  30058  cmtcomlemN  30060  cmt2N  30062  cmtbr2N  30065  cmtbr3N  30066  cmtbr4N  30067  lecmtN  30068  omlfh1N  30070  omlfh3N  30071  meetat  30108  atnle  30129  atlatmstc  30131  hlrelat2  30214  cvrval5  30226  cvrexchlem  30230  cvrexch  30231  cvrat3  30253  cvrat4  30254  ps-2b  30293  2llnmat  30335  2atm  30338  llnmlplnN  30350  2lplnmN  30370  2llnmj  30371  2llnm2N  30379  2llnm4  30381  2lplnm2N  30432  2lplnmj  30433  dalemcea  30471  dalem16  30490  dalem21  30505  dalem54  30537  dalem55  30538  2lnat  30595  2atm2atN  30596  cdlema1N  30602  hlmod1i  30667  atmod1i1m  30669  atmod2i1  30672  atmod2i2  30673  llnmod2i2  30674  atmod4i1  30677  atmod4i2  30678  llnexchb2lem  30679  dalawlem1  30682  dalawlem2  30683  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem9  30690  dalawlem11  30692  dalawlem12  30693  pmapj2N  30740  psubclinN  30759  poml4N  30764  pl42lem1N  30790  pl42lem2N  30791  pl42N  30794  lhpmcvr3  30836  lhpmcvr4N  30837  lhpmcvr5N  30838  lhpmcvr6N  30839  lhpelim  30848  lhpmod2i2  30849  lhpmod6i1  30850  lhprelat3N  30851  lautm  30905  trlval2  30974  trlcl  30975  trlval3  30998  cdlemc1  31002  cdlemc2  31003  cdlemc4  31005  cdlemc5  31006  cdlemc6  31007  cdlemd2  31010  cdleme0aa  31021  cdleme1b  31037  cdleme1  31038  cdleme2  31039  cdleme3b  31040  cdleme3h  31046  cdleme4a  31050  cdleme5  31051  cdleme7e  31058  cdleme7ga  31059  cdleme9b  31063  cdleme11g  31076  cdleme15d  31088  cdleme15  31089  cdleme16b  31090  cdleme16e  31093  cdleme16f  31094  cdleme22gb  31105  cdlemedb  31108  cdleme20j  31129  cdleme22cN  31153  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme23a  31160  cdleme23b  31161  cdleme23c  31162  cdleme28a  31181  cdleme28b  31182  cdleme29ex  31185  cdleme30a  31189  cdlemefr29exN  31213  cdleme32c  31254  cdleme32e  31256  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme42c  31283  cdleme42h  31293  cdleme42i  31294  cdleme48bw  31313  cdlemg7fvbwN  31418  cdlemg10bALTN  31447  cdlemg10  31452  cdlemg11b  31453  cdlemg12f  31459  cdlemg12g  31460  cdlemg17a  31472  trlcolem  31537  cdlemkvcl  31653  cdlemk5u  31672  cdlemk37  31725  cdlemk52  31765  dia2dimlem2  31877  docaclN  31936  doca2N  31938  djajN  31949  cdlemn10  32018  dihjustlem  32028  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord2cN  32033  dihord11b  32034  dihord11c  32036  dihord2pre  32037  dihord2pre2  32038  dihlsscpre  32046  dihvalcq2  32059  dihopelvalcpre  32060  dihord6apre  32068  dihord5b  32071  dihord5apre  32074  dihmeetlem1N  32102  dihglblem5apreN  32103  dihglblem2aN  32105  dihglblem2N  32106  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetbclemN  32116  dihmeetlem3N  32117  dihmeetlem4preN  32118  dihmeetlem6  32121  dihmeetlem7N  32122  dihjatc1  32123  dihjatc2N  32124  dihjatc3  32125  dihmeetlem9N  32127  dihmeetlem16N  32134  dihmeetlem19N  32137  dihmeetcl  32157  dihmeet2  32158  djhlj  32213  dihjatcclem1  32230  dihjatcclem2  32231  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-lat 14168
  Copyright terms: Public domain W3C validator