Theorem latmcl 18425

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ‘cfv 6542  (class class class)co 7414  Basecbs 17173  joincjn 18296  meetcmee 18297  Latclat 18416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-lub 18331  df-glb 18332  df-join 18333  df-meet 18334  df-lat 18417

This theorem is referenced by:  latleeqm1  18452  latmlem1  18454  latmlem12  18456  latnlemlt  18457  latmidm  18459  latabs1  18460  latledi  18462  latmlej11  18463  mod1ile  18478  mod2ile  18479  latdisdlem  18481  oldmm1  38678  oldmj1  38682  latmrot  38693  latm4  38694  olm01  38697  omllaw4  38707  cmtcomlemN  38709  cmt2N  38711  cmtbr2N  38714  cmtbr3N  38715  cmtbr4N  38716  lecmtN  38717  omlfh1N  38719  omlfh3N  38720  meetat  38757  atnle  38778  atlatmstc  38780  hlrelat2  38865  cvrval5  38877  cvrexchlem  38881  cvrexch  38882  cvrat3  38904  cvrat4  38905  ps-2b  38944  2llnmat  38986  2atm  38989  llnmlplnN  39001  2lplnmN  39021  2llnmj  39022  2llnm2N  39030  2llnm4  39032  2lplnm2N  39083  2lplnmj  39084  dalemcea  39122  dalem16  39141  dalem21  39156  dalem54  39188  dalem55  39189  2lnat  39246  2atm2atN  39247  cdlema1N  39253  hlmod1i  39318  atmod1i1m  39320  atmod2i1  39323  atmod2i2  39324  llnmod2i2  39325  atmod4i1  39328  atmod4i2  39329  llnexchb2lem  39330  dalawlem1  39333  dalawlem2  39334  dalawlem3  39335  dalawlem4  39336  dalawlem5  39337  dalawlem6  39338  dalawlem7  39339  dalawlem8  39340  dalawlem9  39341  dalawlem11  39343  dalawlem12  39344  pmapj2N  39391  psubclinN  39410  poml4N  39415  pl42lem1N  39441  pl42lem2N  39442  pl42N  39445  lhpmcvr3  39487  lhpmcvr4N  39488  lhpmcvr5N  39489  lhpmcvr6N  39490  lhpelim  39499  lhpmod2i2  39500  lhpmod6i1  39501  lhprelat3N  39502  lautm  39556  trlval2  39625  trlcl  39626  trlval3  39649  cdlemc1  39653  cdlemc2  39654  cdlemc4  39656  cdlemc5  39657  cdlemc6  39658  cdlemd2  39661  cdleme0aa  39672  cdleme1b  39688  cdleme1  39689  cdleme2  39690  cdleme3b  39691  cdleme3h  39697  cdleme4a  39701  cdleme5  39702  cdleme7e  39709  cdleme7ga  39710  cdleme9b  39714  cdleme11g  39727  cdleme15d  39739  cdleme15  39740  cdleme16b  39741  cdleme16e  39744  cdleme16f  39745  cdleme22gb  39756  cdlemedb  39759  cdleme20j  39780  cdleme22cN  39804  cdleme22e  39806  cdleme22eALTN  39807  cdleme22f  39808  cdleme23a  39811  cdleme23b  39812  cdleme23c  39813  cdleme28a  39832  cdleme28b  39833  cdleme29ex  39836  cdleme30a  39840  cdlemefr29exN  39864  cdleme32c  39905  cdleme32e  39907  cdleme35b  39912  cdleme35c  39913  cdleme35d  39914  cdleme42c  39934  cdleme42h  39944  cdleme42i  39945  cdleme48bw  39964  cdlemg7fvbwN  40069  cdlemg10bALTN  40098  cdlemg10  40103  cdlemg11b  40104  cdlemg12f  40110  cdlemg12g  40111  cdlemg17a  40123  trlcolem  40188  cdlemkvcl  40304  cdlemk5u  40323  cdlemk37  40376  cdlemk52  40416  dia2dimlem2  40527  docaclN  40586  doca2N  40588  djajN  40599  cdlemn10  40668  dihjustlem  40678  dihord1  40680  dihord2a  40681  dihord2b  40682  dihord2cN  40683  dihord11b  40684  dihord11c  40686  dihord2pre  40687  dihord2pre2  40688  dihlsscpre  40696  dihvalcq2  40709  dihopelvalcpre  40710  dihord6apre  40718  dihord5b  40721  dihord5apre  40724  dihmeetlem1N  40752  dihglblem5apreN  40753  dihglblem2aN  40755  dihglblem2N  40756  dihmeetlem2N  40761  dihglbcpreN  40762  dihmeetbclemN  40766  dihmeetlem3N  40767  dihmeetlem4preN  40768  dihmeetlem6  40771  dihmeetlem7N  40772  dihjatc1  40773  dihjatc2N  40774  dihjatc3  40775  dihmeetlem9N  40777  dihmeetlem16N  40784  dihmeetlem19N  40787  dihmeetcl  40807  dihmeet2  40808  djhlj  40863  dihjatcclem1  40880  dihjatcclem2  40881  dihjatcclem4  40883