Theorem latmcl 16241

Description: Closure of meet operation in a lattice. (incom 3598 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 2428	. . 3 |- ( join ` K ) = ( join ` K )
3		latmcl.m	. . 3 |- ./\ = ( meet ` K )
4	1, 2, 3	latlem 16238	. 2 |- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X ( join ` K ) Y ) e. B /\ ( X ./\ Y ) e. B ) )
5	4	simprd 464	1 |- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )

Syntax hints:   -> wi 4   /\ w3a 982   = wceq 1437   e. wcel 1872   ` cfv 5544  (class class class)co 6249   Basecbs 15064   joincjn 16132   meetcmee 16133   Latclat 16234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-lub 16163  df-glb 16164  df-join 16165  df-meet 16166  df-lat 16235

This theorem is referenced by:  latleeqm1  16268  latmlem1  16270  latmlem12  16272  latnlemlt  16273  latmidm  16275  latabs1  16276  latledi  16278  latmlej11  16279  mod1ile  16294  mod2ile  16295  latdisdlem  16378  oldmm1  32695  oldmj1  32699  latmrot  32710  latm4  32711  olm01  32714  omllaw4  32724  cmtcomlemN  32726  cmt2N  32728  cmtbr2N  32731  cmtbr3N  32732  cmtbr4N  32733  lecmtN  32734  omlfh1N  32736  omlfh3N  32737  meetat  32774  atnle  32795  atlatmstc  32797  hlrelat2  32880  cvrval5  32892  cvrexchlem  32896  cvrexch  32897  cvrat3  32919  cvrat4  32920  ps-2b  32959  2llnmat  33001  2atm  33004  llnmlplnN  33016  2lplnmN  33036  2llnmj  33037  2llnm2N  33045  2llnm4  33047  2lplnm2N  33098  2lplnmj  33099  dalemcea  33137  dalem16  33156  dalem21  33171  dalem54  33203  dalem55  33204  2lnat  33261  2atm2atN  33262  cdlema1N  33268  hlmod1i  33333  atmod1i1m  33335  atmod2i1  33338  atmod2i2  33339  llnmod2i2  33340  atmod4i1  33343  atmod4i2  33344  llnexchb2lem  33345  dalawlem1  33348  dalawlem2  33349  dalawlem3  33350  dalawlem4  33351  dalawlem5  33352  dalawlem6  33353  dalawlem7  33354  dalawlem8  33355  dalawlem9  33356  dalawlem11  33358  dalawlem12  33359  pmapj2N  33406  psubclinN  33425  poml4N  33430  pl42lem1N  33456  pl42lem2N  33457  pl42N  33460  lhpmcvr3  33502  lhpmcvr4N  33503  lhpmcvr5N  33504  lhpmcvr6N  33505  lhpelim  33514  lhpmod2i2  33515  lhpmod6i1  33516  lhprelat3N  33517  lautm  33571  trlval2  33641  trlcl  33642  trlval3  33665  cdlemc1  33669  cdlemc2  33670  cdlemc4  33672  cdlemc5  33673  cdlemc6  33674  cdlemd2  33677  cdleme0aa  33688  cdleme1b  33704  cdleme1  33705  cdleme2  33706  cdleme3b  33707  cdleme3h  33713  cdleme4a  33717  cdleme5  33718  cdleme7e  33725  cdleme7ga  33726  cdleme9b  33730  cdleme11g  33743  cdleme15d  33755  cdleme15  33756  cdleme16b  33757  cdleme16e  33760  cdleme16f  33761  cdleme22gb  33772  cdlemedb  33775  cdleme20j  33797  cdleme22cN  33821  cdleme22e  33823  cdleme22eALTN  33824  cdleme22f  33825  cdleme23a  33828  cdleme23b  33829  cdleme23c  33830  cdleme28a  33849  cdleme28b  33850  cdleme29ex  33853  cdleme30a  33857  cdlemefr29exN  33881  cdleme32c  33922  cdleme32e  33924  cdleme35b  33929  cdleme35c  33930  cdleme35d  33931  cdleme42c  33951  cdleme42h  33961  cdleme42i  33962  cdleme48bw  33981  cdlemg7fvbwN  34086  cdlemg10bALTN  34115  cdlemg10  34120  cdlemg11b  34121  cdlemg12f  34127  cdlemg12g  34128  cdlemg17a  34140  trlcolem  34205  cdlemkvcl  34321  cdlemk5u  34340  cdlemk37  34393  cdlemk52  34433  dia2dimlem2  34545  docaclN  34604  doca2N  34606  djajN  34617  cdlemn10  34686  dihjustlem  34696  dihord1  34698  dihord2a  34699  dihord2b  34700  dihord2cN  34701  dihord11b  34702  dihord11c  34704  dihord2pre  34705  dihord2pre2  34706  dihlsscpre  34714  dihvalcq2  34727  dihopelvalcpre  34728  dihord6apre  34736  dihord5b  34739  dihord5apre  34742  dihmeetlem1N  34770  dihglblem5apreN  34771  dihglblem2aN  34773  dihglblem2N  34774  dihmeetlem2N  34779  dihglbcpreN  34780  dihmeetbclemN  34784  dihmeetlem3N  34785  dihmeetlem4preN  34786  dihmeetlem6  34789  dihmeetlem7N  34790  dihjatc1  34791  dihjatc2N  34792  dihjatc3  34793  dihmeetlem9N  34795  dihmeetlem16N  34802  dihmeetlem19N  34805  dihmeetcl  34825  dihmeet2  34826  djhlj  34881  dihjatcclem1  34898  dihjatcclem2  34899  dihjatcclem4  34901