Theorem latmcl 18395

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6490  (class class class)co 7358  Basecbs 17168  joincjn 18266  meetcmee 18267  Latclat 18386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-lat 18387

This theorem is referenced by:  latleeqm1  18422  latmlem1  18424  latmlem12  18426  latnlemlt  18427  latmidm  18429  latabs1  18430  latledi  18432  latmlej11  18433  mod1ile  18448  mod2ile  18449  latdisdlem  18451  oldmm1  39674  oldmj1  39678  latmrot  39689  latm4  39690  olm01  39693  omllaw4  39703  cmtcomlemN  39705  cmt2N  39707  cmtbr2N  39710  cmtbr3N  39711  cmtbr4N  39712  lecmtN  39713  omlfh1N  39715  omlfh3N  39716  meetat  39753  atnle  39774  atlatmstc  39776  hlrelat2  39860  cvrval5  39872  cvrexchlem  39876  cvrexch  39877  cvrat3  39899  cvrat4  39900  ps-2b  39939  2llnmat  39981  2atm  39984  llnmlplnN  39996  2lplnmN  40016  2llnmj  40017  2llnm2N  40025  2llnm4  40027  2lplnm2N  40078  2lplnmj  40079  dalemcea  40117  dalem16  40136  dalem21  40151  dalem54  40183  dalem55  40184  2lnat  40241  2atm2atN  40242  cdlema1N  40248  hlmod1i  40313  atmod1i1m  40315  atmod2i1  40318  atmod2i2  40319  llnmod2i2  40320  atmod4i1  40323  atmod4i2  40324  llnexchb2lem  40325  dalawlem1  40328  dalawlem2  40329  dalawlem3  40330  dalawlem4  40331  dalawlem5  40332  dalawlem6  40333  dalawlem7  40334  dalawlem8  40335  dalawlem9  40336  dalawlem11  40338  dalawlem12  40339  pmapj2N  40386  psubclinN  40405  poml4N  40410  pl42lem1N  40436  pl42lem2N  40437  pl42N  40440  lhpmcvr3  40482  lhpmcvr4N  40483  lhpmcvr5N  40484  lhpmcvr6N  40485  lhpelim  40494  lhpmod2i2  40495  lhpmod6i1  40496  lhprelat3N  40497  lautm  40551  trlval2  40620  trlcl  40621  trlval3  40644  cdlemc1  40648  cdlemc2  40649  cdlemc4  40651  cdlemc5  40652  cdlemc6  40653  cdlemd2  40656  cdleme0aa  40667  cdleme1b  40683  cdleme1  40684  cdleme2  40685  cdleme3b  40686  cdleme3h  40692  cdleme4a  40696  cdleme5  40697  cdleme7e  40704  cdleme7ga  40705  cdleme9b  40709  cdleme11g  40722  cdleme15d  40734  cdleme15  40735  cdleme16b  40736  cdleme16e  40739  cdleme16f  40740  cdleme22gb  40751  cdlemedb  40754  cdleme20j  40775  cdleme22cN  40799  cdleme22e  40801  cdleme22eALTN  40802  cdleme22f  40803  cdleme23a  40806  cdleme23b  40807  cdleme23c  40808  cdleme28a  40827  cdleme28b  40828  cdleme29ex  40831  cdleme30a  40835  cdlemefr29exN  40859  cdleme32c  40900  cdleme32e  40902  cdleme35b  40907  cdleme35c  40908  cdleme35d  40909  cdleme42c  40929  cdleme42h  40939  cdleme42i  40940  cdleme48bw  40959  cdlemg7fvbwN  41064  cdlemg10bALTN  41093  cdlemg10  41098  cdlemg11b  41099  cdlemg12f  41105  cdlemg12g  41106  cdlemg17a  41118  trlcolem  41183  cdlemkvcl  41299  cdlemk5u  41318  cdlemk37  41371  cdlemk52  41411  dia2dimlem2  41522  docaclN  41581  doca2N  41583  djajN  41594  cdlemn10  41663  dihjustlem  41673  dihord1  41675  dihord2a  41676  dihord2b  41677  dihord2cN  41678  dihord11b  41679  dihord11c  41681  dihord2pre  41682  dihord2pre2  41683  dihlsscpre  41691  dihvalcq2  41704  dihopelvalcpre  41705  dihord6apre  41713  dihord5b  41716  dihord5apre  41719  dihmeetlem1N  41747  dihglblem5apreN  41748  dihglblem2aN  41750  dihglblem2N  41751  dihmeetlem2N  41756  dihglbcpreN  41757  dihmeetbclemN  41761  dihmeetlem3N  41762  dihmeetlem4preN  41763  dihmeetlem6  41766  dihmeetlem7N  41767  dihjatc1  41768  dihjatc2N  41769  dihjatc3  41770  dihmeetlem9N  41772  dihmeetlem16N  41779  dihmeetlem19N  41782  dihmeetcl  41802  dihmeet2  41803  djhlj  41858  dihjatcclem1  41875  dihjatcclem2  41876  dihjatcclem4  41878