MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latmcl Structured version   Visualization version   GIF version
Theorem latmcl 18393
Description: Closure of meet operation in a lattice. (incom 4202 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 2733 . . 3 (joinβ€˜πΎ) = (joinβ€˜πΎ)
3 latmcl.m . . 3 ∧ = (meetβ€˜πΎ)
41, 2, 3latlem 18390 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ ((𝑋(joinβ€˜πΎ)π‘Œ) ∈ 𝐡 ∧ (𝑋 ∧ π‘Œ) ∈ 𝐡))
54simprd 497 1 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (𝑋 ∧ π‘Œ) ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  joincjn 18264  meetcmee 18265  Latclat 18384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-lat 18385
This theorem is referenced by:  latleeqm1  18420  latmlem1  18422  latmlem12  18424  latnlemlt  18425  latmidm  18427  latabs1  18428  latledi  18430  latmlej11  18431  mod1ile  18446  mod2ile  18447  latdisdlem  18449  oldmm1  38087  oldmj1  38091  latmrot  38102  latm4  38103  olm01  38106  omllaw4  38116  cmtcomlemN  38118  cmt2N  38120  cmtbr2N  38123  cmtbr3N  38124  cmtbr4N  38125  lecmtN  38126  omlfh1N  38128  omlfh3N  38129  meetat  38166  atnle  38187  atlatmstc  38189  hlrelat2  38274  cvrval5  38286  cvrexchlem  38290  cvrexch  38291  cvrat3  38313  cvrat4  38314  ps-2b  38353  2llnmat  38395  2atm  38398  llnmlplnN  38410  2lplnmN  38430  2llnmj  38431  2llnm2N  38439  2llnm4  38441  2lplnm2N  38492  2lplnmj  38493  dalemcea  38531  dalem16  38550  dalem21  38565  dalem54  38597  dalem55  38598  2lnat  38655  2atm2atN  38656  cdlema1N  38662  hlmod1i  38727  atmod1i1m  38729  atmod2i1  38732  atmod2i2  38733  llnmod2i2  38734  atmod4i1  38737  atmod4i2  38738  llnexchb2lem  38739  dalawlem1  38742  dalawlem2  38743  dalawlem3  38744  dalawlem4  38745  dalawlem5  38746  dalawlem6  38747  dalawlem7  38748  dalawlem8  38749  dalawlem9  38750  dalawlem11  38752  dalawlem12  38753  pmapj2N  38800  psubclinN  38819  poml4N  38824  pl42lem1N  38850  pl42lem2N  38851  pl42N  38854  lhpmcvr3  38896  lhpmcvr4N  38897  lhpmcvr5N  38898  lhpmcvr6N  38899  lhpelim  38908  lhpmod2i2  38909  lhpmod6i1  38910  lhprelat3N  38911  lautm  38965  trlval2  39034  trlcl  39035  trlval3  39058  cdlemc1  39062  cdlemc2  39063  cdlemc4  39065  cdlemc5  39066  cdlemc6  39067  cdlemd2  39070  cdleme0aa  39081  cdleme1b  39097  cdleme1  39098  cdleme2  39099  cdleme3b  39100  cdleme3h  39106  cdleme4a  39110  cdleme5  39111  cdleme7e  39118  cdleme7ga  39119  cdleme9b  39123  cdleme11g  39136  cdleme15d  39148  cdleme15  39149  cdleme16b  39150  cdleme16e  39153  cdleme16f  39154  cdleme22gb  39165  cdlemedb  39168  cdleme20j  39189  cdleme22cN  39213  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme23a  39220  cdleme23b  39221  cdleme23c  39222  cdleme28a  39241  cdleme28b  39242  cdleme29ex  39245  cdleme30a  39249  cdlemefr29exN  39273  cdleme32c  39314  cdleme32e  39316  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme42c  39343  cdleme42h  39353  cdleme42i  39354  cdleme48bw  39373  cdlemg7fvbwN  39478  cdlemg10bALTN  39507  cdlemg10  39512  cdlemg11b  39513  cdlemg12f  39519  cdlemg12g  39520  cdlemg17a  39532  trlcolem  39597  cdlemkvcl  39713  cdlemk5u  39732  cdlemk37  39785  cdlemk52  39825  dia2dimlem2  39936  docaclN  39995  doca2N  39997  djajN  40008  cdlemn10  40077  dihjustlem  40087  dihord1  40089  dihord2a  40090  dihord2b  40091  dihord2cN  40092  dihord11b  40093  dihord11c  40095  dihord2pre  40096  dihord2pre2  40097  dihlsscpre  40105  dihvalcq2  40118  dihopelvalcpre  40119  dihord6apre  40127  dihord5b  40130  dihord5apre  40133  dihmeetlem1N  40161  dihglblem5apreN  40162  dihglblem2aN  40164  dihglblem2N  40165  dihmeetlem2N  40170  dihglbcpreN  40171  dihmeetbclemN  40175  dihmeetlem3N  40176  dihmeetlem4preN  40177  dihmeetlem6  40180  dihmeetlem7N  40181  dihjatc1  40182  dihjatc2N  40183  dihjatc3  40184  dihmeetlem9N  40186  dihmeetlem16N  40193  dihmeetlem19N  40196  dihmeetcl  40216  dihmeet2  40217  djhlj  40272  dihjatcclem1  40289  dihjatcclem2  40290  dihjatcclem4  40292
  Copyright terms: Public domain W3C validator