Theorem latmcl 18346

Description: Closure of meet operation in a lattice. (incom 4160 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 2729	. . 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 1540   ∈ wcel 2109  ‘cfv 6482  (class class class)co 7349  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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  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  39206  oldmj1  39210  latmrot  39221  latm4  39222  olm01  39225  omllaw4  39235  cmtcomlemN  39237  cmt2N  39239  cmtbr2N  39242  cmtbr3N  39243  cmtbr4N  39244  lecmtN  39245  omlfh1N  39247  omlfh3N  39248  meetat  39285  atnle  39306  atlatmstc  39308  hlrelat2  39392  cvrval5  39404  cvrexchlem  39408  cvrexch  39409  cvrat3  39431  cvrat4  39432  ps-2b  39471  2llnmat  39513  2atm  39516  llnmlplnN  39528  2lplnmN  39548  2llnmj  39549  2llnm2N  39557  2llnm4  39559  2lplnm2N  39610  2lplnmj  39611  dalemcea  39649  dalem16  39668  dalem21  39683  dalem54  39715  dalem55  39716  2lnat  39773  2atm2atN  39774  cdlema1N  39780  hlmod1i  39845  atmod1i1m  39847  atmod2i1  39850  atmod2i2  39851  llnmod2i2  39852  atmod4i1  39855  atmod4i2  39856  llnexchb2lem  39857  dalawlem1  39860  dalawlem2  39861  dalawlem3  39862  dalawlem4  39863  dalawlem5  39864  dalawlem6  39865  dalawlem7  39866  dalawlem8  39867  dalawlem9  39868  dalawlem11  39870  dalawlem12  39871  pmapj2N  39918  psubclinN  39937  poml4N  39942  pl42lem1N  39968  pl42lem2N  39969  pl42N  39972  lhpmcvr3  40014  lhpmcvr4N  40015  lhpmcvr5N  40016  lhpmcvr6N  40017  lhpelim  40026  lhpmod2i2  40027  lhpmod6i1  40028  lhprelat3N  40029  lautm  40083  trlval2  40152  trlcl  40153  trlval3  40176  cdlemc1  40180  cdlemc2  40181  cdlemc4  40183  cdlemc5  40184  cdlemc6  40185  cdlemd2  40188  cdleme0aa  40199  cdleme1b  40215  cdleme1  40216  cdleme2  40217  cdleme3b  40218  cdleme3h  40224  cdleme4a  40228  cdleme5  40229  cdleme7e  40236  cdleme7ga  40237  cdleme9b  40241  cdleme11g  40254  cdleme15d  40266  cdleme15  40267  cdleme16b  40268  cdleme16e  40271  cdleme16f  40272  cdleme22gb  40283  cdlemedb  40286  cdleme20j  40307  cdleme22cN  40331  cdleme22e  40333  cdleme22eALTN  40334  cdleme22f  40335  cdleme23a  40338  cdleme23b  40339  cdleme23c  40340  cdleme28a  40359  cdleme28b  40360  cdleme29ex  40363  cdleme30a  40367  cdlemefr29exN  40391  cdleme32c  40432  cdleme32e  40434  cdleme35b  40439  cdleme35c  40440  cdleme35d  40441  cdleme42c  40461  cdleme42h  40471  cdleme42i  40472  cdleme48bw  40491  cdlemg7fvbwN  40596  cdlemg10bALTN  40625  cdlemg10  40630  cdlemg11b  40631  cdlemg12f  40637  cdlemg12g  40638  cdlemg17a  40650  trlcolem  40715  cdlemkvcl  40831  cdlemk5u  40850  cdlemk37  40903  cdlemk52  40943  dia2dimlem2  41054  docaclN  41113  doca2N  41115  djajN  41126  cdlemn10  41195  dihjustlem  41205  dihord1  41207  dihord2a  41208  dihord2b  41209  dihord2cN  41210  dihord11b  41211  dihord11c  41213  dihord2pre  41214  dihord2pre2  41215  dihlsscpre  41223  dihvalcq2  41236  dihopelvalcpre  41237  dihord6apre  41245  dihord5b  41248  dihord5apre  41251  dihmeetlem1N  41279  dihglblem5apreN  41280  dihglblem2aN  41282  dihglblem2N  41283  dihmeetlem2N  41288  dihglbcpreN  41289  dihmeetbclemN  41293  dihmeetlem3N  41294  dihmeetlem4preN  41295  dihmeetlem6  41298  dihmeetlem7N  41299  dihjatc1  41300  dihjatc2N  41301  dihjatc3  41302  dihmeetlem9N  41304  dihmeetlem16N  41311  dihmeetlem19N  41314  dihmeetcl  41334  dihmeet2  41335  djhlj  41390  dihjatcclem1  41407  dihjatcclem2  41408  dihjatcclem4  41410