Theorem latmcl 18496

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ‘cfv 6537  (class class class)co 7411  Basecbs 17269  joincjn 18367  meetcmee 18368  Latclat 18487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-lub 18400  df-glb 18401  df-join 18402  df-meet 18403  df-lat 18488

This theorem is referenced by:  latleeqm1  18523  latmlem1  18525  latmlem12  18527  latnlemlt  18528  latmidm  18530  latabs1  18531  latledi  18533  latmlej11  18534  mod1ile  18549  mod2ile  18550  latdisdlem  18552  oldmm1  39881  oldmj1  39885  latmrot  39896  latm4  39897  olm01  39900  omllaw4  39910  cmtcomlemN  39912  cmt2N  39914  cmtbr2N  39917  cmtbr3N  39918  cmtbr4N  39919  lecmtN  39920  omlfh1N  39922  omlfh3N  39923  meetat  39960  atnle  39981  atlatmstc  39983  hlrelat2  40067  cvrval5  40079  cvrexchlem  40083  cvrexch  40084  cvrat3  40106  cvrat4  40107  ps-2b  40146  2llnmat  40188  2atm  40191  llnmlplnN  40203  2lplnmN  40223  2llnmj  40224  2llnm2N  40232  2llnm4  40234  2lplnm2N  40285  2lplnmj  40286  dalemcea  40324  dalem16  40343  dalem21  40358  dalem54  40390  dalem55  40391  2lnat  40448  2atm2atN  40449  cdlema1N  40455  hlmod1i  40520  atmod1i1m  40522  atmod2i1  40525  atmod2i2  40526  llnmod2i2  40527  atmod4i1  40530  atmod4i2  40531  llnexchb2lem  40532  dalawlem1  40535  dalawlem2  40536  dalawlem3  40537  dalawlem4  40538  dalawlem5  40539  dalawlem6  40540  dalawlem7  40541  dalawlem8  40542  dalawlem9  40543  dalawlem11  40545  dalawlem12  40546  pmapj2N  40593  psubclinN  40612  poml4N  40617  pl42lem1N  40643  pl42lem2N  40644  pl42N  40647  lhpmcvr3  40689  lhpmcvr4N  40690  lhpmcvr5N  40691  lhpmcvr6N  40692  lhpelim  40701  lhpmod2i2  40702  lhpmod6i1  40703  lhprelat3N  40704  lautm  40758  trlval2  40827  trlcl  40828  trlval3  40851  cdlemc1  40855  cdlemc2  40856  cdlemc4  40858  cdlemc5  40859  cdlemc6  40860  cdlemd2  40863  cdleme0aa  40874  cdleme1b  40890  cdleme1  40891  cdleme2  40892  cdleme3b  40893  cdleme3h  40899  cdleme4a  40903  cdleme5  40904  cdleme7e  40911  cdleme7ga  40912  cdleme9b  40916  cdleme11g  40929  cdleme15d  40941  cdleme15  40942  cdleme16b  40943  cdleme16e  40946  cdleme16f  40947  cdleme22gb  40958  cdlemedb  40961  cdleme20j  40982  cdleme22cN  41006  cdleme22e  41008  cdleme22eALTN  41009  cdleme22f  41010  cdleme23a  41013  cdleme23b  41014  cdleme23c  41015  cdleme28a  41034  cdleme28b  41035  cdleme29ex  41038  cdleme30a  41042  cdlemefr29exN  41066  cdleme32c  41107  cdleme32e  41109  cdleme35b  41114  cdleme35c  41115  cdleme35d  41116  cdleme42c  41136  cdleme42h  41146  cdleme42i  41147  cdleme48bw  41166  cdlemg7fvbwN  41271  cdlemg10bALTN  41300  cdlemg10  41305  cdlemg11b  41306  cdlemg12f  41312  cdlemg12g  41313  cdlemg17a  41325  trlcolem  41390  cdlemkvcl  41506  cdlemk5u  41525  cdlemk37  41578  cdlemk52  41618  dia2dimlem2  41729  docaclN  41788  doca2N  41790  djajN  41801  cdlemn10  41870  dihjustlem  41880  dihord1  41882  dihord2a  41883  dihord2b  41884  dihord2cN  41885  dihord11b  41886  dihord11c  41888  dihord2pre  41889  dihord2pre2  41890  dihlsscpre  41898  dihvalcq2  41911  dihopelvalcpre  41912  dihord6apre  41920  dihord5b  41923  dihord5apre  41926  dihmeetlem1N  41954  dihglblem5apreN  41955  dihglblem2aN  41957  dihglblem2N  41958  dihmeetlem2N  41963  dihglbcpreN  41964  dihmeetbclemN  41968  dihmeetlem3N  41969  dihmeetlem4preN  41970  dihmeetlem6  41973  dihmeetlem7N  41974  dihjatc1  41975  dihjatc2N  41976  dihjatc3  41977  dihmeetlem9N  41979  dihmeetlem16N  41986  dihmeetlem19N  41989  dihmeetcl  42009  dihmeet2  42010  djhlj  42065  dihjatcclem1  42082  dihjatcclem2  42083  dihjatcclem4  42085