Theorem latmcl 18472

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

Syntax hints:   → wi 4   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  joincjn 18343  meetcmee 18344  Latclat 18463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-lub 18376  df-glb 18377  df-join 18378  df-meet 18379  df-lat 18464

This theorem is referenced by:  latleeqm1  18499  latmlem1  18501  latmlem12  18503  latnlemlt  18504  latmidm  18506  latabs1  18507  latledi  18509  latmlej11  18510  mod1ile  18525  mod2ile  18526  latdisdlem  18528  oldmm1  39841  oldmj1  39845  latmrot  39856  latm4  39857  olm01  39860  omllaw4  39870  cmtcomlemN  39872  cmt2N  39874  cmtbr2N  39877  cmtbr3N  39878  cmtbr4N  39879  lecmtN  39880  omlfh1N  39882  omlfh3N  39883  meetat  39920  atnle  39941  atlatmstc  39943  hlrelat2  40027  cvrval5  40039  cvrexchlem  40043  cvrexch  40044  cvrat3  40066  cvrat4  40067  ps-2b  40106  2llnmat  40148  2atm  40151  llnmlplnN  40163  2lplnmN  40183  2llnmj  40184  2llnm2N  40192  2llnm4  40194  2lplnm2N  40245  2lplnmj  40246  dalemcea  40284  dalem16  40303  dalem21  40318  dalem54  40350  dalem55  40351  2lnat  40408  2atm2atN  40409  cdlema1N  40415  hlmod1i  40480  atmod1i1m  40482  atmod2i1  40485  atmod2i2  40486  llnmod2i2  40487  atmod4i1  40490  atmod4i2  40491  llnexchb2lem  40492  dalawlem1  40495  dalawlem2  40496  dalawlem3  40497  dalawlem4  40498  dalawlem5  40499  dalawlem6  40500  dalawlem7  40501  dalawlem8  40502  dalawlem9  40503  dalawlem11  40505  dalawlem12  40506  pmapj2N  40553  psubclinN  40572  poml4N  40577  pl42lem1N  40603  pl42lem2N  40604  pl42N  40607  lhpmcvr3  40649  lhpmcvr4N  40650  lhpmcvr5N  40651  lhpmcvr6N  40652  lhpelim  40661  lhpmod2i2  40662  lhpmod6i1  40663  lhprelat3N  40664  lautm  40718  trlval2  40787  trlcl  40788  trlval3  40811  cdlemc1  40815  cdlemc2  40816  cdlemc4  40818  cdlemc5  40819  cdlemc6  40820  cdlemd2  40823  cdleme0aa  40834  cdleme1b  40850  cdleme1  40851  cdleme2  40852  cdleme3b  40853  cdleme3h  40859  cdleme4a  40863  cdleme5  40864  cdleme7e  40871  cdleme7ga  40872  cdleme9b  40876  cdleme11g  40889  cdleme15d  40901  cdleme15  40902  cdleme16b  40903  cdleme16e  40906  cdleme16f  40907  cdleme22gb  40918  cdlemedb  40921  cdleme20j  40942  cdleme22cN  40966  cdleme22e  40968  cdleme22eALTN  40969  cdleme22f  40970  cdleme23a  40973  cdleme23b  40974  cdleme23c  40975  cdleme28a  40994  cdleme28b  40995  cdleme29ex  40998  cdleme30a  41002  cdlemefr29exN  41026  cdleme32c  41067  cdleme32e  41069  cdleme35b  41074  cdleme35c  41075  cdleme35d  41076  cdleme42c  41096  cdleme42h  41106  cdleme42i  41107  cdleme48bw  41126  cdlemg7fvbwN  41231  cdlemg10bALTN  41260  cdlemg10  41265  cdlemg11b  41266  cdlemg12f  41272  cdlemg12g  41273  cdlemg17a  41285  trlcolem  41350  cdlemkvcl  41466  cdlemk5u  41485  cdlemk37  41538  cdlemk52  41578  dia2dimlem2  41689  docaclN  41748  doca2N  41750  djajN  41761  cdlemn10  41830  dihjustlem  41840  dihord1  41842  dihord2a  41843  dihord2b  41844  dihord2cN  41845  dihord11b  41846  dihord11c  41848  dihord2pre  41849  dihord2pre2  41850  dihlsscpre  41858  dihvalcq2  41871  dihopelvalcpre  41872  dihord6apre  41880  dihord5b  41883  dihord5apre  41886  dihmeetlem1N  41914  dihglblem5apreN  41915  dihglblem2aN  41917  dihglblem2N  41918  dihmeetlem2N  41923  dihglbcpreN  41924  dihmeetbclemN  41928  dihmeetlem3N  41929  dihmeetlem4preN  41930  dihmeetlem6  41933  dihmeetlem7N  41934  dihjatc1  41935  dihjatc2N  41936  dihjatc3  41937  dihmeetlem9N  41939  dihmeetlem16N  41946  dihmeetlem19N  41949  dihmeetcl  41969  dihmeet2  41970  djhlj  42025  dihjatcclem1  42042  dihjatcclem2  42043  dihjatcclem4  42045