Theorem latmcl 18073

Description: Closure of meet operation in a lattice. (incom 4131 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 2738	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
3		latmcl.m	. . 3 ⊢ ∧ = (meet‘𝐾)
4	1, 2, 3	latlem 18070	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 495	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  joincjn 17944  meetcmee 17945  Latclat 18064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-lub 17979  df-glb 17980  df-join 17981  df-meet 17982  df-lat 18065

This theorem is referenced by:  latleeqm1  18100  latmlem1  18102  latmlem12  18104  latnlemlt  18105  latmidm  18107  latabs1  18108  latledi  18110  latmlej11  18111  mod1ile  18126  mod2ile  18127  latdisdlem  18129  oldmm1  37158  oldmj1  37162  latmrot  37173  latm4  37174  olm01  37177  omllaw4  37187  cmtcomlemN  37189  cmt2N  37191  cmtbr2N  37194  cmtbr3N  37195  cmtbr4N  37196  lecmtN  37197  omlfh1N  37199  omlfh3N  37200  meetat  37237  atnle  37258  atlatmstc  37260  hlrelat2  37344  cvrval5  37356  cvrexchlem  37360  cvrexch  37361  cvrat3  37383  cvrat4  37384  ps-2b  37423  2llnmat  37465  2atm  37468  llnmlplnN  37480  2lplnmN  37500  2llnmj  37501  2llnm2N  37509  2llnm4  37511  2lplnm2N  37562  2lplnmj  37563  dalemcea  37601  dalem16  37620  dalem21  37635  dalem54  37667  dalem55  37668  2lnat  37725  2atm2atN  37726  cdlema1N  37732  hlmod1i  37797  atmod1i1m  37799  atmod2i1  37802  atmod2i2  37803  llnmod2i2  37804  atmod4i1  37807  atmod4i2  37808  llnexchb2lem  37809  dalawlem1  37812  dalawlem2  37813  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  pmapj2N  37870  psubclinN  37889  poml4N  37894  pl42lem1N  37920  pl42lem2N  37921  pl42N  37924  lhpmcvr3  37966  lhpmcvr4N  37967  lhpmcvr5N  37968  lhpmcvr6N  37969  lhpelim  37978  lhpmod2i2  37979  lhpmod6i1  37980  lhprelat3N  37981  lautm  38035  trlval2  38104  trlcl  38105  trlval3  38128  cdlemc1  38132  cdlemc2  38133  cdlemc4  38135  cdlemc5  38136  cdlemc6  38137  cdlemd2  38140  cdleme0aa  38151  cdleme1b  38167  cdleme1  38168  cdleme2  38169  cdleme3b  38170  cdleme3h  38176  cdleme4a  38180  cdleme5  38181  cdleme7e  38188  cdleme7ga  38189  cdleme9b  38193  cdleme11g  38206  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16e  38223  cdleme16f  38224  cdleme22gb  38235  cdlemedb  38238  cdleme20j  38259  cdleme22cN  38283  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme28a  38311  cdleme28b  38312  cdleme29ex  38315  cdleme30a  38319  cdlemefr29exN  38343  cdleme32c  38384  cdleme32e  38386  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme42c  38413  cdleme42h  38423  cdleme42i  38424  cdleme48bw  38443  cdlemg7fvbwN  38548  cdlemg10bALTN  38577  cdlemg10  38582  cdlemg11b  38583  cdlemg12f  38589  cdlemg12g  38590  cdlemg17a  38602  trlcolem  38667  cdlemkvcl  38783  cdlemk5u  38802  cdlemk37  38855  cdlemk52  38895  dia2dimlem2  39006  docaclN  39065  doca2N  39067  djajN  39078  cdlemn10  39147  dihjustlem  39157  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord2cN  39162  dihord11b  39163  dihord11c  39165  dihord2pre  39166  dihord2pre2  39167  dihlsscpre  39175  dihvalcq2  39188  dihopelvalcpre  39189  dihord6apre  39197  dihord5b  39200  dihord5apre  39203  dihmeetlem1N  39231  dihglblem5apreN  39232  dihglblem2aN  39234  dihglblem2N  39235  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetbclemN  39245  dihmeetlem3N  39246  dihmeetlem4preN  39247  dihmeetlem6  39250  dihmeetlem7N  39251  dihjatc1  39252  dihjatc2N  39253  dihjatc3  39254  dihmeetlem9N  39256  dihmeetlem16N  39263  dihmeetlem19N  39266  dihmeetcl  39286  dihmeet2  39287  djhlj  39342  dihjatcclem1  39359  dihjatcclem2  39360  dihjatcclem4  39362