Theorem latmcl 18399

Description: Closure of meet operation in a lattice. (incom 4172 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 18396	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 495	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  joincjn 18272  meetcmee 18273  Latclat 18390

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 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-lub 18305  df-glb 18306  df-join 18307  df-meet 18308  df-lat 18391

This theorem is referenced by:  latleeqm1  18426  latmlem1  18428  latmlem12  18430  latnlemlt  18431  latmidm  18433  latabs1  18434  latledi  18436  latmlej11  18437  mod1ile  18452  mod2ile  18453  latdisdlem  18455  oldmm1  39210  oldmj1  39214  latmrot  39225  latm4  39226  olm01  39229  omllaw4  39239  cmtcomlemN  39241  cmt2N  39243  cmtbr2N  39246  cmtbr3N  39247  cmtbr4N  39248  lecmtN  39249  omlfh1N  39251  omlfh3N  39252  meetat  39289  atnle  39310  atlatmstc  39312  hlrelat2  39397  cvrval5  39409  cvrexchlem  39413  cvrexch  39414  cvrat3  39436  cvrat4  39437  ps-2b  39476  2llnmat  39518  2atm  39521  llnmlplnN  39533  2lplnmN  39553  2llnmj  39554  2llnm2N  39562  2llnm4  39564  2lplnm2N  39615  2lplnmj  39616  dalemcea  39654  dalem16  39673  dalem21  39688  dalem54  39720  dalem55  39721  2lnat  39778  2atm2atN  39779  cdlema1N  39785  hlmod1i  39850  atmod1i1m  39852  atmod2i1  39855  atmod2i2  39856  llnmod2i2  39857  atmod4i1  39860  atmod4i2  39861  llnexchb2lem  39862  dalawlem1  39865  dalawlem2  39866  dalawlem3  39867  dalawlem4  39868  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  pmapj2N  39923  psubclinN  39942  poml4N  39947  pl42lem1N  39973  pl42lem2N  39974  pl42N  39977  lhpmcvr3  40019  lhpmcvr4N  40020  lhpmcvr5N  40021  lhpmcvr6N  40022  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  lhprelat3N  40034  lautm  40088  trlval2  40157  trlcl  40158  trlval3  40181  cdlemc1  40185  cdlemc2  40186  cdlemc4  40188  cdlemc5  40189  cdlemc6  40190  cdlemd2  40193  cdleme0aa  40204  cdleme1b  40220  cdleme1  40221  cdleme2  40222  cdleme3b  40223  cdleme3h  40229  cdleme4a  40233  cdleme5  40234  cdleme7e  40241  cdleme7ga  40242  cdleme9b  40246  cdleme11g  40259  cdleme15d  40271  cdleme15  40272  cdleme16b  40273  cdleme16e  40276  cdleme16f  40277  cdleme22gb  40288  cdlemedb  40291  cdleme20j  40312  cdleme22cN  40336  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme28a  40364  cdleme28b  40365  cdleme29ex  40368  cdleme30a  40372  cdlemefr29exN  40396  cdleme32c  40437  cdleme32e  40439  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme42c  40466  cdleme42h  40476  cdleme42i  40477  cdleme48bw  40496  cdlemg7fvbwN  40601  cdlemg10bALTN  40630  cdlemg10  40635  cdlemg11b  40636  cdlemg12f  40642  cdlemg12g  40643  cdlemg17a  40655  trlcolem  40720  cdlemkvcl  40836  cdlemk5u  40855  cdlemk37  40908  cdlemk52  40948  dia2dimlem2  41059  docaclN  41118  doca2N  41120  djajN  41131  cdlemn10  41200  dihjustlem  41210  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord2cN  41215  dihord11b  41216  dihord11c  41218  dihord2pre  41219  dihord2pre2  41220  dihlsscpre  41228  dihvalcq2  41241  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihord5apre  41256  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem2aN  41287  dihglblem2N  41288  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetbclemN  41298  dihmeetlem3N  41299  dihmeetlem4preN  41300  dihmeetlem6  41303  dihmeetlem7N  41304  dihjatc1  41305  dihjatc2N  41306  dihjatc3  41307  dihmeetlem9N  41309  dihmeetlem16N  41316  dihmeetlem19N  41319  dihmeetcl  41339  dihmeet2  41340  djhlj  41395  dihjatcclem1  41412  dihjatcclem2  41413  dihjatcclem4  41415