Theorem latmcl 15218

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

Syntax hints:   -> wi 4   /\ w3a 960   = wceq 1364   e. wcel 1761   ` cfv 5415  (class class class)co 6090   Basecbs 14170   joincjn 15110   meetcmee 15111   Latclat 15211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-lub 15140  df-glb 15141  df-join 15142  df-meet 15143  df-lat 15212

This theorem is referenced by:  latleeqm1  15245  latmlem1  15247  latmlem12  15249  latnlemlt  15250  latmidm  15252  latabs1  15253  latledi  15255  latmlej11  15256  mod1ile  15271  mod2ile  15272  latdisdlem  15355  oldmm1  32550  oldmj1  32554  latmrot  32565  latm4  32566  olm01  32569  omllaw4  32579  cmtcomlemN  32581  cmt2N  32583  cmtbr2N  32586  cmtbr3N  32587  cmtbr4N  32588  lecmtN  32589  omlfh1N  32591  omlfh3N  32592  meetat  32629  atnle  32650  atlatmstc  32652  hlrelat2  32735  cvrval5  32747  cvrexchlem  32751  cvrexch  32752  cvrat3  32774  cvrat4  32775  ps-2b  32814  2llnmat  32856  2atm  32859  llnmlplnN  32871  2lplnmN  32891  2llnmj  32892  2llnm2N  32900  2llnm4  32902  2lplnm2N  32953  2lplnmj  32954  dalemcea  32992  dalem16  33011  dalem21  33026  dalem54  33058  dalem55  33059  2lnat  33116  2atm2atN  33117  cdlema1N  33123  hlmod1i  33188  atmod1i1m  33190  atmod2i1  33193  atmod2i2  33194  llnmod2i2  33195  atmod4i1  33198  atmod4i2  33199  llnexchb2lem  33200  dalawlem1  33203  dalawlem2  33204  dalawlem3  33205  dalawlem4  33206  dalawlem5  33207  dalawlem6  33208  dalawlem7  33209  dalawlem8  33210  dalawlem9  33211  dalawlem11  33213  dalawlem12  33214  pmapj2N  33261  psubclinN  33280  poml4N  33285  pl42lem1N  33311  pl42lem2N  33312  pl42N  33315  lhpmcvr3  33357  lhpmcvr4N  33358  lhpmcvr5N  33359  lhpmcvr6N  33360  lhpelim  33369  lhpmod2i2  33370  lhpmod6i1  33371  lhprelat3N  33372  lautm  33426  trlval2  33495  trlcl  33496  trlval3  33519  cdlemc1  33523  cdlemc2  33524  cdlemc4  33526  cdlemc5  33527  cdlemc6  33528  cdlemd2  33531  cdleme0aa  33542  cdleme1b  33558  cdleme1  33559  cdleme2  33560  cdleme3b  33561  cdleme3h  33567  cdleme4a  33571  cdleme5  33572  cdleme7e  33579  cdleme7ga  33580  cdleme9b  33584  cdleme11g  33597  cdleme15d  33609  cdleme15  33610  cdleme16b  33611  cdleme16e  33614  cdleme16f  33615  cdleme22gb  33626  cdlemedb  33629  cdleme20j  33650  cdleme22cN  33674  cdleme22e  33676  cdleme22eALTN  33677  cdleme22f  33678  cdleme23a  33681  cdleme23b  33682  cdleme23c  33683  cdleme28a  33702  cdleme28b  33703  cdleme29ex  33706  cdleme30a  33710  cdlemefr29exN  33734  cdleme32c  33775  cdleme32e  33777  cdleme35b  33782  cdleme35c  33783  cdleme35d  33784  cdleme42c  33804  cdleme42h  33814  cdleme42i  33815  cdleme48bw  33834  cdlemg7fvbwN  33939  cdlemg10bALTN  33968  cdlemg10  33973  cdlemg11b  33974  cdlemg12f  33980  cdlemg12g  33981  cdlemg17a  33993  trlcolem  34058  cdlemkvcl  34174  cdlemk5u  34193  cdlemk37  34246  cdlemk52  34286  dia2dimlem2  34398  docaclN  34457  doca2N  34459  djajN  34470  cdlemn10  34539  dihjustlem  34549  dihord1  34551  dihord2a  34552  dihord2b  34553  dihord2cN  34554  dihord11b  34555  dihord11c  34557  dihord2pre  34558  dihord2pre2  34559  dihlsscpre  34567  dihvalcq2  34580  dihopelvalcpre  34581  dihord6apre  34589  dihord5b  34592  dihord5apre  34595  dihmeetlem1N  34623  dihglblem5apreN  34624  dihglblem2aN  34626  dihglblem2N  34627  dihmeetlem2N  34632  dihglbcpreN  34633  dihmeetbclemN  34637  dihmeetlem3N  34638  dihmeetlem4preN  34639  dihmeetlem6  34642  dihmeetlem7N  34643  dihjatc1  34644  dihjatc2N  34645  dihjatc3  34646  dihmeetlem9N  34648  dihmeetlem16N  34655  dihmeetlem19N  34658  dihmeetcl  34678  dihmeet2  34679  djhlj  34734  dihjatcclem1  34751  dihjatcclem2  34752  dihjatcclem4  34754