Theorem latmcl 18626

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146  ‘cfv 6546  (class class class)co 7427  Basecbs 17399  joincjn 18497  meetcmee 18498  Latclat 18617

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-lub 18530  df-glb 18531  df-join 18532  df-meet 18533  df-lat 18618

This theorem is used by:  latleeqm1  18653  latmlem1  18655  latmlem12  18657  latnlemlt  18658  latmidm  18660  latabs1  18661  latledi  18663  latmlej11  18664  mod1ile  18679  mod2ile  18680  latdisdlem  18682  oldmm1  40414  oldmj1  40418  latmrot  40429  latm4  40430  olm01  40433  omllaw4  40443  cmtcomlemN  40445  cmt2N  40447  cmtbr2N  40450  cmtbr3N  40451  cmtbr4N  40452  lecmtN  40453  omlfh1N  40455  omlfh3N  40456  meetat  40493  atnle  40514  atlatmstc  40516  hlrelat2  40600  cvrval5  40612  cvrexchlem  40616  cvrexch  40617  cvrat3  40639  cvrat4  40640  ps-2b  40679  2llnmat  40721  2atm  40724  llnmlplnN  40736  2lplnmN  40756  2llnmj  40757  2llnm2N  40765  2llnm4  40767  2lplnm2N  40818  2lplnmj  40819  dalemcea  40857  dalem16  40876  dalem21  40891  dalem54  40923  dalem55  40924  2lnat  40981  2atm2atN  40982  cdlema1N  40988  hlmod1i  41053  atmod1i1m  41055  atmod2i1  41058  atmod2i2  41059  llnmod2i2  41060  atmod4i1  41063  atmod4i2  41064  llnexchb2lem  41065  dalawlem1  41068  dalawlem2  41069  dalawlem3  41070  dalawlem4  41071  dalawlem5  41072  dalawlem6  41073  dalawlem7  41074  dalawlem8  41075  dalawlem9  41076  dalawlem11  41078  dalawlem12  41079  pmapj2N  41126  psubclinN  41145  poml4N  41150  pl42lem1N  41176  pl42lem2N  41177  pl42N  41180  lhpmcvr3  41222  lhpmcvr4N  41223  lhpmcvr5N  41224  lhpmcvr6N  41225  lhpelim  41234  lhpmod2i2  41235  lhpmod6i1  41236  lhprelat3N  41237  lautm  41291  trlval2  41360  trlcl  41361  trlval3  41384  cdlemc1  41388  cdlemc2  41389  cdlemc4  41391  cdlemc5  41392  cdlemc6  41393  cdlemd2  41396  cdleme0aa  41407  cdleme1b  41423  cdleme1  41424  cdleme2  41425  cdleme3b  41426  cdleme3h  41432  cdleme4a  41436  cdleme5  41437  cdleme7e  41444  cdleme7ga  41445  cdleme9b  41449  cdleme11g  41462  cdleme15d  41474  cdleme15  41475  cdleme16b  41476  cdleme16e  41479  cdleme16f  41480  cdleme22gb  41491  cdlemedb  41494  cdleme20j  41515  cdleme22cN  41539  cdleme22e  41541  cdleme22eALTN  41542  cdleme22f  41543  cdleme23a  41546  cdleme23b  41547  cdleme23c  41548  cdleme28a  41567  cdleme28b  41568  cdleme29ex  41571  cdleme30a  41575  cdlemefr29exN  41599  cdleme32c  41640  cdleme32e  41642  cdleme35b  41647  cdleme35c  41648  cdleme35d  41649  cdleme42c  41669  cdleme42h  41679  cdleme42i  41680  cdleme48bw  41699  cdlemg7fvbwN  41804  cdlemg10bALTN  41833  cdlemg10  41838  cdlemg11b  41839  cdlemg12f  41845  cdlemg12g  41846  cdlemg17a  41858  trlcolem  41923  cdlemkvcl  42039  cdlemk5u  42058  cdlemk37  42111  cdlemk52  42151  dia2dimlem2  42262  docaclN  42321  doca2N  42323  djajN  42334  cdlemn10  42403  dihjustlem  42413  dihord1  42415  dihord2a  42416  dihord2b  42417  dihord2cN  42418  dihord11b  42419  dihord11c  42421  dihord2pre  42422  dihord2pre2  42423  dihlsscpre  42431  dihvalcq2  42444  dihopelvalcpre  42445  dihord6apre  42453  dihord5b  42456  dihord5apre  42459  dihmeetlem1N  42487  dihglblem5apreN  42488  dihglblem2aN  42490  dihglblem2N  42491  dihmeetlem2N  42496  dihglbcpreN  42497  dihmeetbclemN  42501  dihmeetlem3N  42502  dihmeetlem4preN  42503  dihmeetlem6  42506  dihmeetlem7N  42507  dihjatc1  42508  dihjatc2N  42509  dihjatc3  42510  dihmeetlem9N  42512  dihmeetlem16N  42519  dihmeetlem19N  42522  dihmeetcl  42542  dihmeet2  42543  djhlj  42598  dihjatcclem1  42615  dihjatcclem2  42616  dihjatcclem4  42618