Theorem latmcl 18139

Description: Closure of meet operation in a lattice. (incom 4139 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 18136	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 495	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109  ‘cfv 6430  (class class class)co 7268  Basecbs 16893  joincjn 18010  meetcmee 18011  Latclat 18130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-riota 7225  df-ov 7271  df-oprab 7272  df-lub 18045  df-glb 18046  df-join 18047  df-meet 18048  df-lat 18131

This theorem is referenced by:  latleeqm1  18166  latmlem1  18168  latmlem12  18170  latnlemlt  18171  latmidm  18173  latabs1  18174  latledi  18176  latmlej11  18177  mod1ile  18192  mod2ile  18193  latdisdlem  18195  oldmm1  37210  oldmj1  37214  latmrot  37225  latm4  37226  olm01  37229  omllaw4  37239  cmtcomlemN  37241  cmt2N  37243  cmtbr2N  37246  cmtbr3N  37247  cmtbr4N  37248  lecmtN  37249  omlfh1N  37251  omlfh3N  37252  meetat  37289  atnle  37310  atlatmstc  37312  hlrelat2  37396  cvrval5  37408  cvrexchlem  37412  cvrexch  37413  cvrat3  37435  cvrat4  37436  ps-2b  37475  2llnmat  37517  2atm  37520  llnmlplnN  37532  2lplnmN  37552  2llnmj  37553  2llnm2N  37561  2llnm4  37563  2lplnm2N  37614  2lplnmj  37615  dalemcea  37653  dalem16  37672  dalem21  37687  dalem54  37719  dalem55  37720  2lnat  37777  2atm2atN  37778  cdlema1N  37784  hlmod1i  37849  atmod1i1m  37851  atmod2i1  37854  atmod2i2  37855  llnmod2i2  37856  atmod4i1  37859  atmod4i2  37860  llnexchb2lem  37861  dalawlem1  37864  dalawlem2  37865  dalawlem3  37866  dalawlem4  37867  dalawlem5  37868  dalawlem6  37869  dalawlem7  37870  dalawlem8  37871  dalawlem9  37872  dalawlem11  37874  dalawlem12  37875  pmapj2N  37922  psubclinN  37941  poml4N  37946  pl42lem1N  37972  pl42lem2N  37973  pl42N  37976  lhpmcvr3  38018  lhpmcvr4N  38019  lhpmcvr5N  38020  lhpmcvr6N  38021  lhpelim  38030  lhpmod2i2  38031  lhpmod6i1  38032  lhprelat3N  38033  lautm  38087  trlval2  38156  trlcl  38157  trlval3  38180  cdlemc1  38184  cdlemc2  38185  cdlemc4  38187  cdlemc5  38188  cdlemc6  38189  cdlemd2  38192  cdleme0aa  38203  cdleme1b  38219  cdleme1  38220  cdleme2  38221  cdleme3b  38222  cdleme3h  38228  cdleme4a  38232  cdleme5  38233  cdleme7e  38240  cdleme7ga  38241  cdleme9b  38245  cdleme11g  38258  cdleme15d  38270  cdleme15  38271  cdleme16b  38272  cdleme16e  38275  cdleme16f  38276  cdleme22gb  38287  cdlemedb  38290  cdleme20j  38311  cdleme22cN  38335  cdleme22e  38337  cdleme22eALTN  38338  cdleme22f  38339  cdleme23a  38342  cdleme23b  38343  cdleme23c  38344  cdleme28a  38363  cdleme28b  38364  cdleme29ex  38367  cdleme30a  38371  cdlemefr29exN  38395  cdleme32c  38436  cdleme32e  38438  cdleme35b  38443  cdleme35c  38444  cdleme35d  38445  cdleme42c  38465  cdleme42h  38475  cdleme42i  38476  cdleme48bw  38495  cdlemg7fvbwN  38600  cdlemg10bALTN  38629  cdlemg10  38634  cdlemg11b  38635  cdlemg12f  38641  cdlemg12g  38642  cdlemg17a  38654  trlcolem  38719  cdlemkvcl  38835  cdlemk5u  38854  cdlemk37  38907  cdlemk52  38947  dia2dimlem2  39058  docaclN  39117  doca2N  39119  djajN  39130  cdlemn10  39199  dihjustlem  39209  dihord1  39211  dihord2a  39212  dihord2b  39213  dihord2cN  39214  dihord11b  39215  dihord11c  39217  dihord2pre  39218  dihord2pre2  39219  dihlsscpre  39227  dihvalcq2  39240  dihopelvalcpre  39241  dihord6apre  39249  dihord5b  39252  dihord5apre  39255  dihmeetlem1N  39283  dihglblem5apreN  39284  dihglblem2aN  39286  dihglblem2N  39287  dihmeetlem2N  39292  dihglbcpreN  39293  dihmeetbclemN  39297  dihmeetlem3N  39298  dihmeetlem4preN  39299  dihmeetlem6  39302  dihmeetlem7N  39303  dihjatc1  39304  dihjatc2N  39305  dihjatc3  39306  dihmeetlem9N  39308  dihmeetlem16N  39315  dihmeetlem19N  39318  dihmeetcl  39338  dihmeet2  39339  djhlj  39394  dihjatcclem1  39411  dihjatcclem2  39412  dihjatcclem4  39414