Theorem latmcl 18406

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  joincjn 18279  meetcmee 18280  Latclat 18397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-lub 18312  df-glb 18313  df-join 18314  df-meet 18315  df-lat 18398

This theorem is referenced by:  latleeqm1  18433  latmlem1  18435  latmlem12  18437  latnlemlt  18438  latmidm  18440  latabs1  18441  latledi  18443  latmlej11  18444  mod1ile  18459  mod2ile  18460  latdisdlem  18462  oldmm1  39217  oldmj1  39221  latmrot  39232  latm4  39233  olm01  39236  omllaw4  39246  cmtcomlemN  39248  cmt2N  39250  cmtbr2N  39253  cmtbr3N  39254  cmtbr4N  39255  lecmtN  39256  omlfh1N  39258  omlfh3N  39259  meetat  39296  atnle  39317  atlatmstc  39319  hlrelat2  39404  cvrval5  39416  cvrexchlem  39420  cvrexch  39421  cvrat3  39443  cvrat4  39444  ps-2b  39483  2llnmat  39525  2atm  39528  llnmlplnN  39540  2lplnmN  39560  2llnmj  39561  2llnm2N  39569  2llnm4  39571  2lplnm2N  39622  2lplnmj  39623  dalemcea  39661  dalem16  39680  dalem21  39695  dalem54  39727  dalem55  39728  2lnat  39785  2atm2atN  39786  cdlema1N  39792  hlmod1i  39857  atmod1i1m  39859  atmod2i1  39862  atmod2i2  39863  llnmod2i2  39864  atmod4i1  39867  atmod4i2  39868  llnexchb2lem  39869  dalawlem1  39872  dalawlem2  39873  dalawlem3  39874  dalawlem4  39875  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  pmapj2N  39930  psubclinN  39949  poml4N  39954  pl42lem1N  39980  pl42lem2N  39981  pl42N  39984  lhpmcvr3  40026  lhpmcvr4N  40027  lhpmcvr5N  40028  lhpmcvr6N  40029  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  lhprelat3N  40041  lautm  40095  trlval2  40164  trlcl  40165  trlval3  40188  cdlemc1  40192  cdlemc2  40193  cdlemc4  40195  cdlemc5  40196  cdlemc6  40197  cdlemd2  40200  cdleme0aa  40211  cdleme1b  40227  cdleme1  40228  cdleme2  40229  cdleme3b  40230  cdleme3h  40236  cdleme4a  40240  cdleme5  40241  cdleme7e  40248  cdleme7ga  40249  cdleme9b  40253  cdleme11g  40266  cdleme15d  40278  cdleme15  40279  cdleme16b  40280  cdleme16e  40283  cdleme16f  40284  cdleme22gb  40295  cdlemedb  40298  cdleme20j  40319  cdleme22cN  40343  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme23a  40350  cdleme23b  40351  cdleme23c  40352  cdleme28a  40371  cdleme28b  40372  cdleme29ex  40375  cdleme30a  40379  cdlemefr29exN  40403  cdleme32c  40444  cdleme32e  40446  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme42c  40473  cdleme42h  40483  cdleme42i  40484  cdleme48bw  40503  cdlemg7fvbwN  40608  cdlemg10bALTN  40637  cdlemg10  40642  cdlemg11b  40643  cdlemg12f  40649  cdlemg12g  40650  cdlemg17a  40662  trlcolem  40727  cdlemkvcl  40843  cdlemk5u  40862  cdlemk37  40915  cdlemk52  40955  dia2dimlem2  41066  docaclN  41125  doca2N  41127  djajN  41138  cdlemn10  41207  dihjustlem  41217  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord2cN  41222  dihord11b  41223  dihord11c  41225  dihord2pre  41226  dihord2pre2  41227  dihlsscpre  41235  dihvalcq2  41248  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihord5apre  41263  dihmeetlem1N  41291  dihglblem5apreN  41292  dihglblem2aN  41294  dihglblem2N  41295  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetbclemN  41305  dihmeetlem3N  41306  dihmeetlem4preN  41307  dihmeetlem6  41310  dihmeetlem7N  41311  dihjatc1  41312  dihjatc2N  41313  dihjatc3  41314  dihmeetlem9N  41316  dihmeetlem16N  41323  dihmeetlem19N  41326  dihmeetcl  41346  dihmeet2  41347  djhlj  41402  dihjatcclem1  41419  dihjatcclem2  41420  dihjatcclem4  41422