Theorem latmcl 18397

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

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  (class class class)co 7356  Basecbs 17170  joincjn 18268  meetcmee 18269  Latclat 18388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-lat 18389

This theorem is referenced by:  latleeqm1  18424  latmlem1  18426  latmlem12  18428  latnlemlt  18429  latmidm  18431  latabs1  18432  latledi  18434  latmlej11  18435  mod1ile  18450  mod2ile  18451  latdisdlem  18453  oldmm1  39709  oldmj1  39713  latmrot  39724  latm4  39725  olm01  39728  omllaw4  39738  cmtcomlemN  39740  cmt2N  39742  cmtbr2N  39745  cmtbr3N  39746  cmtbr4N  39747  lecmtN  39748  omlfh1N  39750  omlfh3N  39751  meetat  39788  atnle  39809  atlatmstc  39811  hlrelat2  39895  cvrval5  39907  cvrexchlem  39911  cvrexch  39912  cvrat3  39934  cvrat4  39935  ps-2b  39974  2llnmat  40016  2atm  40019  llnmlplnN  40031  2lplnmN  40051  2llnmj  40052  2llnm2N  40060  2llnm4  40062  2lplnm2N  40113  2lplnmj  40114  dalemcea  40152  dalem16  40171  dalem21  40186  dalem54  40218  dalem55  40219  2lnat  40276  2atm2atN  40277  cdlema1N  40283  hlmod1i  40348  atmod1i1m  40350  atmod2i1  40353  atmod2i2  40354  llnmod2i2  40355  atmod4i1  40358  atmod4i2  40359  llnexchb2lem  40360  dalawlem1  40363  dalawlem2  40364  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  pmapj2N  40421  psubclinN  40440  poml4N  40445  pl42lem1N  40471  pl42lem2N  40472  pl42N  40475  lhpmcvr3  40517  lhpmcvr4N  40518  lhpmcvr5N  40519  lhpmcvr6N  40520  lhpelim  40529  lhpmod2i2  40530  lhpmod6i1  40531  lhprelat3N  40532  lautm  40586  trlval2  40655  trlcl  40656  trlval3  40679  cdlemc1  40683  cdlemc2  40684  cdlemc4  40686  cdlemc5  40687  cdlemc6  40688  cdlemd2  40691  cdleme0aa  40702  cdleme1b  40718  cdleme1  40719  cdleme2  40720  cdleme3b  40721  cdleme3h  40727  cdleme4a  40731  cdleme5  40732  cdleme7e  40739  cdleme7ga  40740  cdleme9b  40744  cdleme11g  40757  cdleme15d  40769  cdleme15  40770  cdleme16b  40771  cdleme16e  40774  cdleme16f  40775  cdleme22gb  40786  cdlemedb  40789  cdleme20j  40810  cdleme22cN  40834  cdleme22e  40836  cdleme22eALTN  40837  cdleme22f  40838  cdleme23a  40841  cdleme23b  40842  cdleme23c  40843  cdleme28a  40862  cdleme28b  40863  cdleme29ex  40866  cdleme30a  40870  cdlemefr29exN  40894  cdleme32c  40935  cdleme32e  40937  cdleme35b  40942  cdleme35c  40943  cdleme35d  40944  cdleme42c  40964  cdleme42h  40974  cdleme42i  40975  cdleme48bw  40994  cdlemg7fvbwN  41099  cdlemg10bALTN  41128  cdlemg10  41133  cdlemg11b  41134  cdlemg12f  41140  cdlemg12g  41141  cdlemg17a  41153  trlcolem  41218  cdlemkvcl  41334  cdlemk5u  41353  cdlemk37  41406  cdlemk52  41446  dia2dimlem2  41557  docaclN  41616  doca2N  41618  djajN  41629  cdlemn10  41698  dihjustlem  41708  dihord1  41710  dihord2a  41711  dihord2b  41712  dihord2cN  41713  dihord11b  41714  dihord11c  41716  dihord2pre  41717  dihord2pre2  41718  dihlsscpre  41726  dihvalcq2  41739  dihopelvalcpre  41740  dihord6apre  41748  dihord5b  41751  dihord5apre  41754  dihmeetlem1N  41782  dihglblem5apreN  41783  dihglblem2aN  41785  dihglblem2N  41786  dihmeetlem2N  41791  dihglbcpreN  41792  dihmeetbclemN  41796  dihmeetlem3N  41797  dihmeetlem4preN  41798  dihmeetlem6  41801  dihmeetlem7N  41802  dihjatc1  41803  dihjatc2N  41804  dihjatc3  41805  dihmeetlem9N  41807  dihmeetlem16N  41814  dihmeetlem19N  41817  dihmeetcl  41837  dihmeet2  41838  djhlj  41893  dihjatcclem1  41910  dihjatcclem2  41911  dihjatcclem4  41913