Theorem latmcl 18167

Description: Closure of meet operation in a lattice. (incom 4136 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

Step	Hyp	Ref	Expression
1		latmcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		eqid 2739	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
3		latmcl.m	. . 3 ⊢ ∧ = (meet‘𝐾)
4	1, 2, 3	latlem 18164	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 496	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  joincjn 18038  meetcmee 18039  Latclat 18158

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 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-lub 18073  df-glb 18074  df-join 18075  df-meet 18076  df-lat 18159

This theorem is referenced by:  latleeqm1  18194  latmlem1  18196  latmlem12  18198  latnlemlt  18199  latmidm  18201  latabs1  18202  latledi  18204  latmlej11  18205  mod1ile  18220  mod2ile  18221  latdisdlem  18223  oldmm1  37238  oldmj1  37242  latmrot  37253  latm4  37254  olm01  37257  omllaw4  37267  cmtcomlemN  37269  cmt2N  37271  cmtbr2N  37274  cmtbr3N  37275  cmtbr4N  37276  lecmtN  37277  omlfh1N  37279  omlfh3N  37280  meetat  37317  atnle  37338  atlatmstc  37340  hlrelat2  37424  cvrval5  37436  cvrexchlem  37440  cvrexch  37441  cvrat3  37463  cvrat4  37464  ps-2b  37503  2llnmat  37545  2atm  37548  llnmlplnN  37560  2lplnmN  37580  2llnmj  37581  2llnm2N  37589  2llnm4  37591  2lplnm2N  37642  2lplnmj  37643  dalemcea  37681  dalem16  37700  dalem21  37715  dalem54  37747  dalem55  37748  2lnat  37805  2atm2atN  37806  cdlema1N  37812  hlmod1i  37877  atmod1i1m  37879  atmod2i1  37882  atmod2i2  37883  llnmod2i2  37884  atmod4i1  37887  atmod4i2  37888  llnexchb2lem  37889  dalawlem1  37892  dalawlem2  37893  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  pmapj2N  37950  psubclinN  37969  poml4N  37974  pl42lem1N  38000  pl42lem2N  38001  pl42N  38004  lhpmcvr3  38046  lhpmcvr4N  38047  lhpmcvr5N  38048  lhpmcvr6N  38049  lhpelim  38058  lhpmod2i2  38059  lhpmod6i1  38060  lhprelat3N  38061  lautm  38115  trlval2  38184  trlcl  38185  trlval3  38208  cdlemc1  38212  cdlemc2  38213  cdlemc4  38215  cdlemc5  38216  cdlemc6  38217  cdlemd2  38220  cdleme0aa  38231  cdleme1b  38247  cdleme1  38248  cdleme2  38249  cdleme3b  38250  cdleme3h  38256  cdleme4a  38260  cdleme5  38261  cdleme7e  38268  cdleme7ga  38269  cdleme9b  38273  cdleme11g  38286  cdleme15d  38298  cdleme15  38299  cdleme16b  38300  cdleme16e  38303  cdleme16f  38304  cdleme22gb  38315  cdlemedb  38318  cdleme20j  38339  cdleme22cN  38363  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme23a  38370  cdleme23b  38371  cdleme23c  38372  cdleme28a  38391  cdleme28b  38392  cdleme29ex  38395  cdleme30a  38399  cdlemefr29exN  38423  cdleme32c  38464  cdleme32e  38466  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme42c  38493  cdleme42h  38503  cdleme42i  38504  cdleme48bw  38523  cdlemg7fvbwN  38628  cdlemg10bALTN  38657  cdlemg10  38662  cdlemg11b  38663  cdlemg12f  38669  cdlemg12g  38670  cdlemg17a  38682  trlcolem  38747  cdlemkvcl  38863  cdlemk5u  38882  cdlemk37  38935  cdlemk52  38975  dia2dimlem2  39086  docaclN  39145  doca2N  39147  djajN  39158  cdlemn10  39227  dihjustlem  39237  dihord1  39239  dihord2a  39240  dihord2b  39241  dihord2cN  39242  dihord11b  39243  dihord11c  39245  dihord2pre  39246  dihord2pre2  39247  dihlsscpre  39255  dihvalcq2  39268  dihopelvalcpre  39269  dihord6apre  39277  dihord5b  39280  dihord5apre  39283  dihmeetlem1N  39311  dihglblem5apreN  39312  dihglblem2aN  39314  dihglblem2N  39315  dihmeetlem2N  39320  dihglbcpreN  39321  dihmeetbclemN  39325  dihmeetlem3N  39326  dihmeetlem4preN  39327  dihmeetlem6  39330  dihmeetlem7N  39331  dihjatc1  39332  dihjatc2N  39333  dihjatc3  39334  dihmeetlem9N  39336  dihmeetlem16N  39343  dihmeetlem19N  39346  dihmeetcl  39366  dihmeet2  39367  djhlj  39422  dihjatcclem1  39439  dihjatcclem2  39440  dihjatcclem4  39442