Theorem latmcl 18491

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  Basecbs 17264  joincjn 18362  meetcmee 18363  Latclat 18482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-lub 18395  df-glb 18396  df-join 18397  df-meet 18398  df-lat 18483

This theorem is referenced by:  latleeqm1  18518  latmlem1  18520  latmlem12  18522  latnlemlt  18523  latmidm  18525  latabs1  18526  latledi  18528  latmlej11  18529  mod1ile  18544  mod2ile  18545  latdisdlem  18547  oldmm1  40011  oldmj1  40015  latmrot  40026  latm4  40027  olm01  40030  omllaw4  40040  cmtcomlemN  40042  cmt2N  40044  cmtbr2N  40047  cmtbr3N  40048  cmtbr4N  40049  lecmtN  40050  omlfh1N  40052  omlfh3N  40053  meetat  40090  atnle  40111  atlatmstc  40113  hlrelat2  40197  cvrval5  40209  cvrexchlem  40213  cvrexch  40214  cvrat3  40236  cvrat4  40237  ps-2b  40276  2llnmat  40318  2atm  40321  llnmlplnN  40333  2lplnmN  40353  2llnmj  40354  2llnm2N  40362  2llnm4  40364  2lplnm2N  40415  2lplnmj  40416  dalemcea  40454  dalem16  40473  dalem21  40488  dalem54  40520  dalem55  40521  2lnat  40578  2atm2atN  40579  cdlema1N  40585  hlmod1i  40650  atmod1i1m  40652  atmod2i1  40655  atmod2i2  40656  llnmod2i2  40657  atmod4i1  40660  atmod4i2  40661  llnexchb2lem  40662  dalawlem1  40665  dalawlem2  40666  dalawlem3  40667  dalawlem4  40668  dalawlem5  40669  dalawlem6  40670  dalawlem7  40671  dalawlem8  40672  dalawlem9  40673  dalawlem11  40675  dalawlem12  40676  pmapj2N  40723  psubclinN  40742  poml4N  40747  pl42lem1N  40773  pl42lem2N  40774  pl42N  40777  lhpmcvr3  40819  lhpmcvr4N  40820  lhpmcvr5N  40821  lhpmcvr6N  40822  lhpelim  40831  lhpmod2i2  40832  lhpmod6i1  40833  lhprelat3N  40834  lautm  40888  trlval2  40957  trlcl  40958  trlval3  40981  cdlemc1  40985  cdlemc2  40986  cdlemc4  40988  cdlemc5  40989  cdlemc6  40990  cdlemd2  40993  cdleme0aa  41004  cdleme1b  41020  cdleme1  41021  cdleme2  41022  cdleme3b  41023  cdleme3h  41029  cdleme4a  41033  cdleme5  41034  cdleme7e  41041  cdleme7ga  41042  cdleme9b  41046  cdleme11g  41059  cdleme15d  41071  cdleme15  41072  cdleme16b  41073  cdleme16e  41076  cdleme16f  41077  cdleme22gb  41088  cdlemedb  41091  cdleme20j  41112  cdleme22cN  41136  cdleme22e  41138  cdleme22eALTN  41139  cdleme22f  41140  cdleme23a  41143  cdleme23b  41144  cdleme23c  41145  cdleme28a  41164  cdleme28b  41165  cdleme29ex  41168  cdleme30a  41172  cdlemefr29exN  41196  cdleme32c  41237  cdleme32e  41239  cdleme35b  41244  cdleme35c  41245  cdleme35d  41246  cdleme42c  41266  cdleme42h  41276  cdleme42i  41277  cdleme48bw  41296  cdlemg7fvbwN  41401  cdlemg10bALTN  41430  cdlemg10  41435  cdlemg11b  41436  cdlemg12f  41442  cdlemg12g  41443  cdlemg17a  41455  trlcolem  41520  cdlemkvcl  41636  cdlemk5u  41655  cdlemk37  41708  cdlemk52  41748  dia2dimlem2  41859  docaclN  41918  doca2N  41920  djajN  41931  cdlemn10  42000  dihjustlem  42010  dihord1  42012  dihord2a  42013  dihord2b  42014  dihord2cN  42015  dihord11b  42016  dihord11c  42018  dihord2pre  42019  dihord2pre2  42020  dihlsscpre  42028  dihvalcq2  42041  dihopelvalcpre  42042  dihord6apre  42050  dihord5b  42053  dihord5apre  42056  dihmeetlem1N  42084  dihglblem5apreN  42085  dihglblem2aN  42087  dihglblem2N  42088  dihmeetlem2N  42093  dihglbcpreN  42094  dihmeetbclemN  42098  dihmeetlem3N  42099  dihmeetlem4preN  42100  dihmeetlem6  42103  dihmeetlem7N  42104  dihjatc1  42105  dihjatc2N  42106  dihjatc3  42107  dihmeetlem9N  42109  dihmeetlem16N  42116  dihmeetlem19N  42119  dihmeetcl  42139  dihmeet2  42140  djhlj  42195  dihjatcclem1  42212  dihjatcclem2  42213  dihjatcclem4  42215