Theorem latmcl 17520

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

Syntax hints:   → wi 4   ∧ w3a 1068   = wceq 1507   ∈ wcel 2050  ‘cfv 6188  (class class class)co 6976  Basecbs 16339  joincjn 17412  meetcmee 17413  Latclat 17513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-lub 17442  df-glb 17443  df-join 17444  df-meet 17445  df-lat 17514

This theorem is referenced by:  latleeqm1  17547  latmlem1  17549  latmlem12  17551  latnlemlt  17552  latmidm  17554  latabs1  17555  latledi  17557  latmlej11  17558  mod1ile  17573  mod2ile  17574  latdisdlem  17657  oldmm1  35804  oldmj1  35808  latmrot  35819  latm4  35820  olm01  35823  omllaw4  35833  cmtcomlemN  35835  cmt2N  35837  cmtbr2N  35840  cmtbr3N  35841  cmtbr4N  35842  lecmtN  35843  omlfh1N  35845  omlfh3N  35846  meetat  35883  atnle  35904  atlatmstc  35906  hlrelat2  35990  cvrval5  36002  cvrexchlem  36006  cvrexch  36007  cvrat3  36029  cvrat4  36030  ps-2b  36069  2llnmat  36111  2atm  36114  llnmlplnN  36126  2lplnmN  36146  2llnmj  36147  2llnm2N  36155  2llnm4  36157  2lplnm2N  36208  2lplnmj  36209  dalemcea  36247  dalem16  36266  dalem21  36281  dalem54  36313  dalem55  36314  2lnat  36371  2atm2atN  36372  cdlema1N  36378  hlmod1i  36443  atmod1i1m  36445  atmod2i1  36448  atmod2i2  36449  llnmod2i2  36450  atmod4i1  36453  atmod4i2  36454  llnexchb2lem  36455  dalawlem1  36458  dalawlem2  36459  dalawlem3  36460  dalawlem4  36461  dalawlem5  36462  dalawlem6  36463  dalawlem7  36464  dalawlem8  36465  dalawlem9  36466  dalawlem11  36468  dalawlem12  36469  pmapj2N  36516  psubclinN  36535  poml4N  36540  pl42lem1N  36566  pl42lem2N  36567  pl42N  36570  lhpmcvr3  36612  lhpmcvr4N  36613  lhpmcvr5N  36614  lhpmcvr6N  36615  lhpelim  36624  lhpmod2i2  36625  lhpmod6i1  36626  lhprelat3N  36627  lautm  36681  trlval2  36750  trlcl  36751  trlval3  36774  cdlemc1  36778  cdlemc2  36779  cdlemc4  36781  cdlemc5  36782  cdlemc6  36783  cdlemd2  36786  cdleme0aa  36797  cdleme1b  36813  cdleme1  36814  cdleme2  36815  cdleme3b  36816  cdleme3h  36822  cdleme4a  36826  cdleme5  36827  cdleme7e  36834  cdleme7ga  36835  cdleme9b  36839  cdleme11g  36852  cdleme15d  36864  cdleme15  36865  cdleme16b  36866  cdleme16e  36869  cdleme16f  36870  cdleme22gb  36881  cdlemedb  36884  cdleme20j  36905  cdleme22cN  36929  cdleme22e  36931  cdleme22eALTN  36932  cdleme22f  36933  cdleme23a  36936  cdleme23b  36937  cdleme23c  36938  cdleme28a  36957  cdleme28b  36958  cdleme29ex  36961  cdleme30a  36965  cdlemefr29exN  36989  cdleme32c  37030  cdleme32e  37032  cdleme35b  37037  cdleme35c  37038  cdleme35d  37039  cdleme42c  37059  cdleme42h  37069  cdleme42i  37070  cdleme48bw  37089  cdlemg7fvbwN  37194  cdlemg10bALTN  37223  cdlemg10  37228  cdlemg11b  37229  cdlemg12f  37235  cdlemg12g  37236  cdlemg17a  37248  trlcolem  37313  cdlemkvcl  37429  cdlemk5u  37448  cdlemk37  37501  cdlemk52  37541  dia2dimlem2  37652  docaclN  37711  doca2N  37713  djajN  37724  cdlemn10  37793  dihjustlem  37803  dihord1  37805  dihord2a  37806  dihord2b  37807  dihord2cN  37808  dihord11b  37809  dihord11c  37811  dihord2pre  37812  dihord2pre2  37813  dihlsscpre  37821  dihvalcq2  37834  dihopelvalcpre  37835  dihord6apre  37843  dihord5b  37846  dihord5apre  37849  dihmeetlem1N  37877  dihglblem5apreN  37878  dihglblem2aN  37880  dihglblem2N  37881  dihmeetlem2N  37886  dihglbcpreN  37887  dihmeetbclemN  37891  dihmeetlem3N  37892  dihmeetlem4preN  37893  dihmeetlem6  37896  dihmeetlem7N  37897  dihjatc1  37898  dihjatc2N  37899  dihjatc3  37900  dihmeetlem9N  37902  dihmeetlem16N  37909  dihmeetlem19N  37912  dihmeetcl  37932  dihmeet2  37933  djhlj  37988  dihjatcclem1  38005  dihjatcclem2  38006  dihjatcclem4  38008