Theorem latmcl 16347

Description: Closure of meet operation in a lattice. (incom 3637 analog.) (Contributed by NM, 14-Sep-2011.)

Hypotheses

Ref	Expression
latmcl.b	|- B = ( Base ` K )
latmcl.m	|- ./\ = ( meet ` K )

Assertion

Ref	Expression
latmcl	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )

Proof of Theorem latmcl

Step	Hyp	Ref	Expression
1		latmcl.b	. . 3 |- B = ( Base ` K )
2		eqid 2462	. . 3 |- ( join ` K ) = ( join ` K )
3		latmcl.m	. . 3 |- ./\ = ( meet ` K )
4	1, 2, 3	latlem 16344	. 2 |- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X ( join ` K ) Y ) e. B /\ ( X ./\ Y ) e. B ) )
5	4	simprd 469	1 |- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )

Syntax hints:   -> wi 4   /\ w3a 991   = wceq 1455   e. wcel 1898   ` cfv 5601  (class class class)co 6315   Basecbs 15170   joincjn 16238   meetcmee 16239   Latclat 16340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-lub 16269  df-glb 16270  df-join 16271  df-meet 16272  df-lat 16341

This theorem is referenced by:  latleeqm1  16374  latmlem1  16376  latmlem12  16378  latnlemlt  16379  latmidm  16381  latabs1  16382  latledi  16384  latmlej11  16385  mod1ile  16400  mod2ile  16401  latdisdlem  16484  oldmm1  32828  oldmj1  32832  latmrot  32843  latm4  32844  olm01  32847  omllaw4  32857  cmtcomlemN  32859  cmt2N  32861  cmtbr2N  32864  cmtbr3N  32865  cmtbr4N  32866  lecmtN  32867  omlfh1N  32869  omlfh3N  32870  meetat  32907  atnle  32928  atlatmstc  32930  hlrelat2  33013  cvrval5  33025  cvrexchlem  33029  cvrexch  33030  cvrat3  33052  cvrat4  33053  ps-2b  33092  2llnmat  33134  2atm  33137  llnmlplnN  33149  2lplnmN  33169  2llnmj  33170  2llnm2N  33178  2llnm4  33180  2lplnm2N  33231  2lplnmj  33232  dalemcea  33270  dalem16  33289  dalem21  33304  dalem54  33336  dalem55  33337  2lnat  33394  2atm2atN  33395  cdlema1N  33401  hlmod1i  33466  atmod1i1m  33468  atmod2i1  33471  atmod2i2  33472  llnmod2i2  33473  atmod4i1  33476  atmod4i2  33477  llnexchb2lem  33478  dalawlem1  33481  dalawlem2  33482  dalawlem3  33483  dalawlem4  33484  dalawlem5  33485  dalawlem6  33486  dalawlem7  33487  dalawlem8  33488  dalawlem9  33489  dalawlem11  33491  dalawlem12  33492  pmapj2N  33539  psubclinN  33558  poml4N  33563  pl42lem1N  33589  pl42lem2N  33590  pl42N  33593  lhpmcvr3  33635  lhpmcvr4N  33636  lhpmcvr5N  33637  lhpmcvr6N  33638  lhpelim  33647  lhpmod2i2  33648  lhpmod6i1  33649  lhprelat3N  33650  lautm  33704  trlval2  33774  trlcl  33775  trlval3  33798  cdlemc1  33802  cdlemc2  33803  cdlemc4  33805  cdlemc5  33806  cdlemc6  33807  cdlemd2  33810  cdleme0aa  33821  cdleme1b  33837  cdleme1  33838  cdleme2  33839  cdleme3b  33840  cdleme3h  33846  cdleme4a  33850  cdleme5  33851  cdleme7e  33858  cdleme7ga  33859  cdleme9b  33863  cdleme11g  33876  cdleme15d  33888  cdleme15  33889  cdleme16b  33890  cdleme16e  33893  cdleme16f  33894  cdleme22gb  33905  cdlemedb  33908  cdleme20j  33930  cdleme22cN  33954  cdleme22e  33956  cdleme22eALTN  33957  cdleme22f  33958  cdleme23a  33961  cdleme23b  33962  cdleme23c  33963  cdleme28a  33982  cdleme28b  33983  cdleme29ex  33986  cdleme30a  33990  cdlemefr29exN  34014  cdleme32c  34055  cdleme32e  34057  cdleme35b  34062  cdleme35c  34063  cdleme35d  34064  cdleme42c  34084  cdleme42h  34094  cdleme42i  34095  cdleme48bw  34114  cdlemg7fvbwN  34219  cdlemg10bALTN  34248  cdlemg10  34253  cdlemg11b  34254  cdlemg12f  34260  cdlemg12g  34261  cdlemg17a  34273  trlcolem  34338  cdlemkvcl  34454  cdlemk5u  34473  cdlemk37  34526  cdlemk52  34566  dia2dimlem2  34678  docaclN  34737  doca2N  34739  djajN  34750  cdlemn10  34819  dihjustlem  34829  dihord1  34831  dihord2a  34832  dihord2b  34833  dihord2cN  34834  dihord11b  34835  dihord11c  34837  dihord2pre  34838  dihord2pre2  34839  dihlsscpre  34847  dihvalcq2  34860  dihopelvalcpre  34861  dihord6apre  34869  dihord5b  34872  dihord5apre  34875  dihmeetlem1N  34903  dihglblem5apreN  34904  dihglblem2aN  34906  dihglblem2N  34907  dihmeetlem2N  34912  dihglbcpreN  34913  dihmeetbclemN  34917  dihmeetlem3N  34918  dihmeetlem4preN  34919  dihmeetlem6  34922  dihmeetlem7N  34923  dihjatc1  34924  dihjatc2N  34925  dihjatc3  34926  dihmeetlem9N  34928  dihmeetlem16N  34935  dihmeetlem19N  34938  dihmeetcl  34958  dihmeet2  34959  djhlj  35014  dihjatcclem1  35031  dihjatcclem2  35032  dihjatcclem4  35034