Theorem latmcl 18346

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  joincjn 18217  meetcmee 18218  Latclat 18337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-lub 18250  df-glb 18251  df-join 18252  df-meet 18253  df-lat 18338

This theorem is referenced by:  latleeqm1  18373  latmlem1  18375  latmlem12  18377  latnlemlt  18378  latmidm  18380  latabs1  18381  latledi  18383  latmlej11  18384  mod1ile  18399  mod2ile  18400  latdisdlem  18402  oldmm1  39326  oldmj1  39330  latmrot  39341  latm4  39342  olm01  39345  omllaw4  39355  cmtcomlemN  39357  cmt2N  39359  cmtbr2N  39362  cmtbr3N  39363  cmtbr4N  39364  lecmtN  39365  omlfh1N  39367  omlfh3N  39368  meetat  39405  atnle  39426  atlatmstc  39428  hlrelat2  39512  cvrval5  39524  cvrexchlem  39528  cvrexch  39529  cvrat3  39551  cvrat4  39552  ps-2b  39591  2llnmat  39633  2atm  39636  llnmlplnN  39648  2lplnmN  39668  2llnmj  39669  2llnm2N  39677  2llnm4  39679  2lplnm2N  39730  2lplnmj  39731  dalemcea  39769  dalem16  39788  dalem21  39803  dalem54  39835  dalem55  39836  2lnat  39893  2atm2atN  39894  cdlema1N  39900  hlmod1i  39965  atmod1i1m  39967  atmod2i1  39970  atmod2i2  39971  llnmod2i2  39972  atmod4i1  39975  atmod4i2  39976  llnexchb2lem  39977  dalawlem1  39980  dalawlem2  39981  dalawlem3  39982  dalawlem4  39983  dalawlem5  39984  dalawlem6  39985  dalawlem7  39986  dalawlem8  39987  dalawlem9  39988  dalawlem11  39990  dalawlem12  39991  pmapj2N  40038  psubclinN  40057  poml4N  40062  pl42lem1N  40088  pl42lem2N  40089  pl42N  40092  lhpmcvr3  40134  lhpmcvr4N  40135  lhpmcvr5N  40136  lhpmcvr6N  40137  lhpelim  40146  lhpmod2i2  40147  lhpmod6i1  40148  lhprelat3N  40149  lautm  40203  trlval2  40272  trlcl  40273  trlval3  40296  cdlemc1  40300  cdlemc2  40301  cdlemc4  40303  cdlemc5  40304  cdlemc6  40305  cdlemd2  40308  cdleme0aa  40319  cdleme1b  40335  cdleme1  40336  cdleme2  40337  cdleme3b  40338  cdleme3h  40344  cdleme4a  40348  cdleme5  40349  cdleme7e  40356  cdleme7ga  40357  cdleme9b  40361  cdleme11g  40374  cdleme15d  40386  cdleme15  40387  cdleme16b  40388  cdleme16e  40391  cdleme16f  40392  cdleme22gb  40403  cdlemedb  40406  cdleme20j  40427  cdleme22cN  40451  cdleme22e  40453  cdleme22eALTN  40454  cdleme22f  40455  cdleme23a  40458  cdleme23b  40459  cdleme23c  40460  cdleme28a  40479  cdleme28b  40480  cdleme29ex  40483  cdleme30a  40487  cdlemefr29exN  40511  cdleme32c  40552  cdleme32e  40554  cdleme35b  40559  cdleme35c  40560  cdleme35d  40561  cdleme42c  40581  cdleme42h  40591  cdleme42i  40592  cdleme48bw  40611  cdlemg7fvbwN  40716  cdlemg10bALTN  40745  cdlemg10  40750  cdlemg11b  40751  cdlemg12f  40757  cdlemg12g  40758  cdlemg17a  40770  trlcolem  40835  cdlemkvcl  40951  cdlemk5u  40970  cdlemk37  41023  cdlemk52  41063  dia2dimlem2  41174  docaclN  41233  doca2N  41235  djajN  41246  cdlemn10  41315  dihjustlem  41325  dihord1  41327  dihord2a  41328  dihord2b  41329  dihord2cN  41330  dihord11b  41331  dihord11c  41333  dihord2pre  41334  dihord2pre2  41335  dihlsscpre  41343  dihvalcq2  41356  dihopelvalcpre  41357  dihord6apre  41365  dihord5b  41368  dihord5apre  41371  dihmeetlem1N  41399  dihglblem5apreN  41400  dihglblem2aN  41402  dihglblem2N  41403  dihmeetlem2N  41408  dihglbcpreN  41409  dihmeetbclemN  41413  dihmeetlem3N  41414  dihmeetlem4preN  41415  dihmeetlem6  41418  dihmeetlem7N  41419  dihjatc1  41420  dihjatc2N  41421  dihjatc3  41422  dihmeetlem9N  41424  dihmeetlem16N  41431  dihmeetlem19N  41434  dihmeetcl  41454  dihmeet2  41455  djhlj  41510  dihjatcclem1  41527  dihjatcclem2  41528  dihjatcclem4  41530