Theorem latmcl 18400

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  (class class class)co 7361  Basecbs 17173  joincjn 18271  meetcmee 18272  Latclat 18391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-lub 18304  df-glb 18305  df-join 18306  df-meet 18307  df-lat 18392

This theorem is referenced by:  latleeqm1  18427  latmlem1  18429  latmlem12  18431  latnlemlt  18432  latmidm  18434  latabs1  18435  latledi  18437  latmlej11  18438  mod1ile  18453  mod2ile  18454  latdisdlem  18456  oldmm1  39680  oldmj1  39684  latmrot  39695  latm4  39696  olm01  39699  omllaw4  39709  cmtcomlemN  39711  cmt2N  39713  cmtbr2N  39716  cmtbr3N  39717  cmtbr4N  39718  lecmtN  39719  omlfh1N  39721  omlfh3N  39722  meetat  39759  atnle  39780  atlatmstc  39782  hlrelat2  39866  cvrval5  39878  cvrexchlem  39882  cvrexch  39883  cvrat3  39905  cvrat4  39906  ps-2b  39945  2llnmat  39987  2atm  39990  llnmlplnN  40002  2lplnmN  40022  2llnmj  40023  2llnm2N  40031  2llnm4  40033  2lplnm2N  40084  2lplnmj  40085  dalemcea  40123  dalem16  40142  dalem21  40157  dalem54  40189  dalem55  40190  2lnat  40247  2atm2atN  40248  cdlema1N  40254  hlmod1i  40319  atmod1i1m  40321  atmod2i1  40324  atmod2i2  40325  llnmod2i2  40326  atmod4i1  40329  atmod4i2  40330  llnexchb2lem  40331  dalawlem1  40334  dalawlem2  40335  dalawlem3  40336  dalawlem4  40337  dalawlem5  40338  dalawlem6  40339  dalawlem7  40340  dalawlem8  40341  dalawlem9  40342  dalawlem11  40344  dalawlem12  40345  pmapj2N  40392  psubclinN  40411  poml4N  40416  pl42lem1N  40442  pl42lem2N  40443  pl42N  40446  lhpmcvr3  40488  lhpmcvr4N  40489  lhpmcvr5N  40490  lhpmcvr6N  40491  lhpelim  40500  lhpmod2i2  40501  lhpmod6i1  40502  lhprelat3N  40503  lautm  40557  trlval2  40626  trlcl  40627  trlval3  40650  cdlemc1  40654  cdlemc2  40655  cdlemc4  40657  cdlemc5  40658  cdlemc6  40659  cdlemd2  40662  cdleme0aa  40673  cdleme1b  40689  cdleme1  40690  cdleme2  40691  cdleme3b  40692  cdleme3h  40698  cdleme4a  40702  cdleme5  40703  cdleme7e  40710  cdleme7ga  40711  cdleme9b  40715  cdleme11g  40728  cdleme15d  40740  cdleme15  40741  cdleme16b  40742  cdleme16e  40745  cdleme16f  40746  cdleme22gb  40757  cdlemedb  40760  cdleme20j  40781  cdleme22cN  40805  cdleme22e  40807  cdleme22eALTN  40808  cdleme22f  40809  cdleme23a  40812  cdleme23b  40813  cdleme23c  40814  cdleme28a  40833  cdleme28b  40834  cdleme29ex  40837  cdleme30a  40841  cdlemefr29exN  40865  cdleme32c  40906  cdleme32e  40908  cdleme35b  40913  cdleme35c  40914  cdleme35d  40915  cdleme42c  40935  cdleme42h  40945  cdleme42i  40946  cdleme48bw  40965  cdlemg7fvbwN  41070  cdlemg10bALTN  41099  cdlemg10  41104  cdlemg11b  41105  cdlemg12f  41111  cdlemg12g  41112  cdlemg17a  41124  trlcolem  41189  cdlemkvcl  41305  cdlemk5u  41324  cdlemk37  41377  cdlemk52  41417  dia2dimlem2  41528  docaclN  41587  doca2N  41589  djajN  41600  cdlemn10  41669  dihjustlem  41679  dihord1  41681  dihord2a  41682  dihord2b  41683  dihord2cN  41684  dihord11b  41685  dihord11c  41687  dihord2pre  41688  dihord2pre2  41689  dihlsscpre  41697  dihvalcq2  41710  dihopelvalcpre  41711  dihord6apre  41719  dihord5b  41722  dihord5apre  41725  dihmeetlem1N  41753  dihglblem5apreN  41754  dihglblem2aN  41756  dihglblem2N  41757  dihmeetlem2N  41762  dihglbcpreN  41763  dihmeetbclemN  41767  dihmeetlem3N  41768  dihmeetlem4preN  41769  dihmeetlem6  41772  dihmeetlem7N  41773  dihjatc1  41774  dihjatc2N  41775  dihjatc3  41776  dihmeetlem9N  41778  dihmeetlem16N  41785  dihmeetlem19N  41788  dihmeetcl  41808  dihmeet2  41809  djhlj  41864  dihjatcclem1  41881  dihjatcclem2  41882  dihjatcclem4  41884