Theorem latmcl 17662

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  joincjn 17554  meetcmee 17555  Latclat 17655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-lub 17584  df-glb 17585  df-join 17586  df-meet 17587  df-lat 17656

This theorem is referenced by:  latleeqm1  17689  latmlem1  17691  latmlem12  17693  latnlemlt  17694  latmidm  17696  latabs1  17697  latledi  17699  latmlej11  17700  mod1ile  17715  mod2ile  17716  latdisdlem  17799  oldmm1  36368  oldmj1  36372  latmrot  36383  latm4  36384  olm01  36387  omllaw4  36397  cmtcomlemN  36399  cmt2N  36401  cmtbr2N  36404  cmtbr3N  36405  cmtbr4N  36406  lecmtN  36407  omlfh1N  36409  omlfh3N  36410  meetat  36447  atnle  36468  atlatmstc  36470  hlrelat2  36554  cvrval5  36566  cvrexchlem  36570  cvrexch  36571  cvrat3  36593  cvrat4  36594  ps-2b  36633  2llnmat  36675  2atm  36678  llnmlplnN  36690  2lplnmN  36710  2llnmj  36711  2llnm2N  36719  2llnm4  36721  2lplnm2N  36772  2lplnmj  36773  dalemcea  36811  dalem16  36830  dalem21  36845  dalem54  36877  dalem55  36878  2lnat  36935  2atm2atN  36936  cdlema1N  36942  hlmod1i  37007  atmod1i1m  37009  atmod2i1  37012  atmod2i2  37013  llnmod2i2  37014  atmod4i1  37017  atmod4i2  37018  llnexchb2lem  37019  dalawlem1  37022  dalawlem2  37023  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  pmapj2N  37080  psubclinN  37099  poml4N  37104  pl42lem1N  37130  pl42lem2N  37131  pl42N  37134  lhpmcvr3  37176  lhpmcvr4N  37177  lhpmcvr5N  37178  lhpmcvr6N  37179  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  lhprelat3N  37191  lautm  37245  trlval2  37314  trlcl  37315  trlval3  37338  cdlemc1  37342  cdlemc2  37343  cdlemc4  37345  cdlemc5  37346  cdlemc6  37347  cdlemd2  37350  cdleme0aa  37361  cdleme1b  37377  cdleme1  37378  cdleme2  37379  cdleme3b  37380  cdleme3h  37386  cdleme4a  37390  cdleme5  37391  cdleme7e  37398  cdleme7ga  37399  cdleme9b  37403  cdleme11g  37416  cdleme15d  37428  cdleme15  37429  cdleme16b  37430  cdleme16e  37433  cdleme16f  37434  cdleme22gb  37445  cdlemedb  37448  cdleme20j  37469  cdleme22cN  37493  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme23a  37500  cdleme23b  37501  cdleme23c  37502  cdleme28a  37521  cdleme28b  37522  cdleme29ex  37525  cdleme30a  37529  cdlemefr29exN  37553  cdleme32c  37594  cdleme32e  37596  cdleme35b  37601  cdleme35c  37602  cdleme35d  37603  cdleme42c  37623  cdleme42h  37633  cdleme42i  37634  cdleme48bw  37653  cdlemg7fvbwN  37758  cdlemg10bALTN  37787  cdlemg10  37792  cdlemg11b  37793  cdlemg12f  37799  cdlemg12g  37800  cdlemg17a  37812  trlcolem  37877  cdlemkvcl  37993  cdlemk5u  38012  cdlemk37  38065  cdlemk52  38105  dia2dimlem2  38216  docaclN  38275  doca2N  38277  djajN  38288  cdlemn10  38357  dihjustlem  38367  dihord1  38369  dihord2a  38370  dihord2b  38371  dihord2cN  38372  dihord11b  38373  dihord11c  38375  dihord2pre  38376  dihord2pre2  38377  dihlsscpre  38385  dihvalcq2  38398  dihopelvalcpre  38399  dihord6apre  38407  dihord5b  38410  dihord5apre  38413  dihmeetlem1N  38441  dihglblem5apreN  38442  dihglblem2aN  38444  dihglblem2N  38445  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetbclemN  38455  dihmeetlem3N  38456  dihmeetlem4preN  38457  dihmeetlem6  38460  dihmeetlem7N  38461  dihjatc1  38462  dihjatc2N  38463  dihjatc3  38464  dihmeetlem9N  38466  dihmeetlem16N  38473  dihmeetlem19N  38476  dihmeetcl  38496  dihmeet2  38497  djhlj  38552  dihjatcclem1  38569  dihjatcclem2  38570  dihjatcclem4  38572