Theorem latmcl 18520

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  (class class class)co 7419  Basecbs 17293  joincjn 18391  meetcmee 18392  Latclat 18511

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-lub 18424  df-glb 18425  df-join 18426  df-meet 18427  df-lat 18512

This theorem is used by:  latleeqm1  18547  latmlem1  18549  latmlem12  18551  latnlemlt  18552  latmidm  18554  latabs1  18555  latledi  18557  latmlej11  18558  mod1ile  18573  mod2ile  18574  latdisdlem  18576  oldmm1  40051  oldmj1  40055  latmrot  40066  latm4  40067  olm01  40070  omllaw4  40080  cmtcomlemN  40082  cmt2N  40084  cmtbr2N  40087  cmtbr3N  40088  cmtbr4N  40089  lecmtN  40090  omlfh1N  40092  omlfh3N  40093  meetat  40130  atnle  40151  atlatmstc  40153  hlrelat2  40237  cvrval5  40249  cvrexchlem  40253  cvrexch  40254  cvrat3  40276  cvrat4  40277  ps-2b  40316  2llnmat  40358  2atm  40361  llnmlplnN  40373  2lplnmN  40393  2llnmj  40394  2llnm2N  40402  2llnm4  40404  2lplnm2N  40455  2lplnmj  40456  dalemcea  40494  dalem16  40513  dalem21  40528  dalem54  40560  dalem55  40561  2lnat  40618  2atm2atN  40619  cdlema1N  40625  hlmod1i  40690  atmod1i1m  40692  atmod2i1  40695  atmod2i2  40696  llnmod2i2  40697  atmod4i1  40700  atmod4i2  40701  llnexchb2lem  40702  dalawlem1  40705  dalawlem2  40706  dalawlem3  40707  dalawlem4  40708  dalawlem5  40709  dalawlem6  40710  dalawlem7  40711  dalawlem8  40712  dalawlem9  40713  dalawlem11  40715  dalawlem12  40716  pmapj2N  40763  psubclinN  40782  poml4N  40787  pl42lem1N  40813  pl42lem2N  40814  pl42N  40817  lhpmcvr3  40859  lhpmcvr4N  40860  lhpmcvr5N  40861  lhpmcvr6N  40862  lhpelim  40871  lhpmod2i2  40872  lhpmod6i1  40873  lhprelat3N  40874  lautm  40928  trlval2  40997  trlcl  40998  trlval3  41021  cdlemc1  41025  cdlemc2  41026  cdlemc4  41028  cdlemc5  41029  cdlemc6  41030  cdlemd2  41033  cdleme0aa  41044  cdleme1b  41060  cdleme1  41061  cdleme2  41062  cdleme3b  41063  cdleme3h  41069  cdleme4a  41073  cdleme5  41074  cdleme7e  41081  cdleme7ga  41082  cdleme9b  41086  cdleme11g  41099  cdleme15d  41111  cdleme15  41112  cdleme16b  41113  cdleme16e  41116  cdleme16f  41117  cdleme22gb  41128  cdlemedb  41131  cdleme20j  41152  cdleme22cN  41176  cdleme22e  41178  cdleme22eALTN  41179  cdleme22f  41180  cdleme23a  41183  cdleme23b  41184  cdleme23c  41185  cdleme28a  41204  cdleme28b  41205  cdleme29ex  41208  cdleme30a  41212  cdlemefr29exN  41236  cdleme32c  41277  cdleme32e  41279  cdleme35b  41284  cdleme35c  41285  cdleme35d  41286  cdleme42c  41306  cdleme42h  41316  cdleme42i  41317  cdleme48bw  41336  cdlemg7fvbwN  41441  cdlemg10bALTN  41470  cdlemg10  41475  cdlemg11b  41476  cdlemg12f  41482  cdlemg12g  41483  cdlemg17a  41495  trlcolem  41560  cdlemkvcl  41676  cdlemk5u  41695  cdlemk37  41748  cdlemk52  41788  dia2dimlem2  41899  docaclN  41958  doca2N  41960  djajN  41971  cdlemn10  42040  dihjustlem  42050  dihord1  42052  dihord2a  42053  dihord2b  42054  dihord2cN  42055  dihord11b  42056  dihord11c  42058  dihord2pre  42059  dihord2pre2  42060  dihlsscpre  42068  dihvalcq2  42081  dihopelvalcpre  42082  dihord6apre  42090  dihord5b  42093  dihord5apre  42096  dihmeetlem1N  42124  dihglblem5apreN  42125  dihglblem2aN  42127  dihglblem2N  42128  dihmeetlem2N  42133  dihglbcpreN  42134  dihmeetbclemN  42138  dihmeetlem3N  42139  dihmeetlem4preN  42140  dihmeetlem6  42143  dihmeetlem7N  42144  dihjatc1  42145  dihjatc2N  42146  dihjatc3  42147  dihmeetlem9N  42149  dihmeetlem16N  42156  dihmeetlem19N  42159  dihmeetcl  42179  dihmeet2  42180  djhlj  42235  dihjatcclem1  42252  dihjatcclem2  42253  dihjatcclem4  42255