Theorem latmcl 18381

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  joincjn 18252  meetcmee 18253  Latclat 18372

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 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-lub 18285  df-glb 18286  df-join 18287  df-meet 18288  df-lat 18373

This theorem is referenced by:  latleeqm1  18408  latmlem1  18410  latmlem12  18412  latnlemlt  18413  latmidm  18415  latabs1  18416  latledi  18418  latmlej11  18419  mod1ile  18434  mod2ile  18435  latdisdlem  18437  oldmm1  39203  oldmj1  39207  latmrot  39218  latm4  39219  olm01  39222  omllaw4  39232  cmtcomlemN  39234  cmt2N  39236  cmtbr2N  39239  cmtbr3N  39240  cmtbr4N  39241  lecmtN  39242  omlfh1N  39244  omlfh3N  39245  meetat  39282  atnle  39303  atlatmstc  39305  hlrelat2  39390  cvrval5  39402  cvrexchlem  39406  cvrexch  39407  cvrat3  39429  cvrat4  39430  ps-2b  39469  2llnmat  39511  2atm  39514  llnmlplnN  39526  2lplnmN  39546  2llnmj  39547  2llnm2N  39555  2llnm4  39557  2lplnm2N  39608  2lplnmj  39609  dalemcea  39647  dalem16  39666  dalem21  39681  dalem54  39713  dalem55  39714  2lnat  39771  2atm2atN  39772  cdlema1N  39778  hlmod1i  39843  atmod1i1m  39845  atmod2i1  39848  atmod2i2  39849  llnmod2i2  39850  atmod4i1  39853  atmod4i2  39854  llnexchb2lem  39855  dalawlem1  39858  dalawlem2  39859  dalawlem3  39860  dalawlem4  39861  dalawlem5  39862  dalawlem6  39863  dalawlem7  39864  dalawlem8  39865  dalawlem9  39866  dalawlem11  39868  dalawlem12  39869  pmapj2N  39916  psubclinN  39935  poml4N  39940  pl42lem1N  39966  pl42lem2N  39967  pl42N  39970  lhpmcvr3  40012  lhpmcvr4N  40013  lhpmcvr5N  40014  lhpmcvr6N  40015  lhpelim  40024  lhpmod2i2  40025  lhpmod6i1  40026  lhprelat3N  40027  lautm  40081  trlval2  40150  trlcl  40151  trlval3  40174  cdlemc1  40178  cdlemc2  40179  cdlemc4  40181  cdlemc5  40182  cdlemc6  40183  cdlemd2  40186  cdleme0aa  40197  cdleme1b  40213  cdleme1  40214  cdleme2  40215  cdleme3b  40216  cdleme3h  40222  cdleme4a  40226  cdleme5  40227  cdleme7e  40234  cdleme7ga  40235  cdleme9b  40239  cdleme11g  40252  cdleme15d  40264  cdleme15  40265  cdleme16b  40266  cdleme16e  40269  cdleme16f  40270  cdleme22gb  40281  cdlemedb  40284  cdleme20j  40305  cdleme22cN  40329  cdleme22e  40331  cdleme22eALTN  40332  cdleme22f  40333  cdleme23a  40336  cdleme23b  40337  cdleme23c  40338  cdleme28a  40357  cdleme28b  40358  cdleme29ex  40361  cdleme30a  40365  cdlemefr29exN  40389  cdleme32c  40430  cdleme32e  40432  cdleme35b  40437  cdleme35c  40438  cdleme35d  40439  cdleme42c  40459  cdleme42h  40469  cdleme42i  40470  cdleme48bw  40489  cdlemg7fvbwN  40594  cdlemg10bALTN  40623  cdlemg10  40628  cdlemg11b  40629  cdlemg12f  40635  cdlemg12g  40636  cdlemg17a  40648  trlcolem  40713  cdlemkvcl  40829  cdlemk5u  40848  cdlemk37  40901  cdlemk52  40941  dia2dimlem2  41052  docaclN  41111  doca2N  41113  djajN  41124  cdlemn10  41193  dihjustlem  41203  dihord1  41205  dihord2a  41206  dihord2b  41207  dihord2cN  41208  dihord11b  41209  dihord11c  41211  dihord2pre  41212  dihord2pre2  41213  dihlsscpre  41221  dihvalcq2  41234  dihopelvalcpre  41235  dihord6apre  41243  dihord5b  41246  dihord5apre  41249  dihmeetlem1N  41277  dihglblem5apreN  41278  dihglblem2aN  41280  dihglblem2N  41281  dihmeetlem2N  41286  dihglbcpreN  41287  dihmeetbclemN  41291  dihmeetlem3N  41292  dihmeetlem4preN  41293  dihmeetlem6  41296  dihmeetlem7N  41297  dihjatc1  41298  dihjatc2N  41299  dihjatc3  41300  dihmeetlem9N  41302  dihmeetlem16N  41309  dihmeetlem19N  41312  dihmeetcl  41332  dihmeet2  41333  djhlj  41388  dihjatcclem1  41405  dihjatcclem2  41406  dihjatcclem4  41408