Theorem latmcl 15222

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

Syntax hints:   -> wi 4   /\ w3a 965   = wceq 1369   e. wcel 1756   ` cfv 5418  (class class class)co 6091   Basecbs 14174   joincjn 15114   meetcmee 15115   Latclat 15215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-lub 15144  df-glb 15145  df-join 15146  df-meet 15147  df-lat 15216

This theorem is referenced by:  latleeqm1  15249  latmlem1  15251  latmlem12  15253  latnlemlt  15254  latmidm  15256  latabs1  15257  latledi  15259  latmlej11  15260  mod1ile  15275  mod2ile  15276  latdisdlem  15359  oldmm1  32862  oldmj1  32866  latmrot  32877  latm4  32878  olm01  32881  omllaw4  32891  cmtcomlemN  32893  cmt2N  32895  cmtbr2N  32898  cmtbr3N  32899  cmtbr4N  32900  lecmtN  32901  omlfh1N  32903  omlfh3N  32904  meetat  32941  atnle  32962  atlatmstc  32964  hlrelat2  33047  cvrval5  33059  cvrexchlem  33063  cvrexch  33064  cvrat3  33086  cvrat4  33087  ps-2b  33126  2llnmat  33168  2atm  33171  llnmlplnN  33183  2lplnmN  33203  2llnmj  33204  2llnm2N  33212  2llnm4  33214  2lplnm2N  33265  2lplnmj  33266  dalemcea  33304  dalem16  33323  dalem21  33338  dalem54  33370  dalem55  33371  2lnat  33428  2atm2atN  33429  cdlema1N  33435  hlmod1i  33500  atmod1i1m  33502  atmod2i1  33505  atmod2i2  33506  llnmod2i2  33507  atmod4i1  33510  atmod4i2  33511  llnexchb2lem  33512  dalawlem1  33515  dalawlem2  33516  dalawlem3  33517  dalawlem4  33518  dalawlem5  33519  dalawlem6  33520  dalawlem7  33521  dalawlem8  33522  dalawlem9  33523  dalawlem11  33525  dalawlem12  33526  pmapj2N  33573  psubclinN  33592  poml4N  33597  pl42lem1N  33623  pl42lem2N  33624  pl42N  33627  lhpmcvr3  33669  lhpmcvr4N  33670  lhpmcvr5N  33671  lhpmcvr6N  33672  lhpelim  33681  lhpmod2i2  33682  lhpmod6i1  33683  lhprelat3N  33684  lautm  33738  trlval2  33807  trlcl  33808  trlval3  33831  cdlemc1  33835  cdlemc2  33836  cdlemc4  33838  cdlemc5  33839  cdlemc6  33840  cdlemd2  33843  cdleme0aa  33854  cdleme1b  33870  cdleme1  33871  cdleme2  33872  cdleme3b  33873  cdleme3h  33879  cdleme4a  33883  cdleme5  33884  cdleme7e  33891  cdleme7ga  33892  cdleme9b  33896  cdleme11g  33909  cdleme15d  33921  cdleme15  33922  cdleme16b  33923  cdleme16e  33926  cdleme16f  33927  cdleme22gb  33938  cdlemedb  33941  cdleme20j  33962  cdleme22cN  33986  cdleme22e  33988  cdleme22eALTN  33989  cdleme22f  33990  cdleme23a  33993  cdleme23b  33994  cdleme23c  33995  cdleme28a  34014  cdleme28b  34015  cdleme29ex  34018  cdleme30a  34022  cdlemefr29exN  34046  cdleme32c  34087  cdleme32e  34089  cdleme35b  34094  cdleme35c  34095  cdleme35d  34096  cdleme42c  34116  cdleme42h  34126  cdleme42i  34127  cdleme48bw  34146  cdlemg7fvbwN  34251  cdlemg10bALTN  34280  cdlemg10  34285  cdlemg11b  34286  cdlemg12f  34292  cdlemg12g  34293  cdlemg17a  34305  trlcolem  34370  cdlemkvcl  34486  cdlemk5u  34505  cdlemk37  34558  cdlemk52  34598  dia2dimlem2  34710  docaclN  34769  doca2N  34771  djajN  34782  cdlemn10  34851  dihjustlem  34861  dihord1  34863  dihord2a  34864  dihord2b  34865  dihord2cN  34866  dihord11b  34867  dihord11c  34869  dihord2pre  34870  dihord2pre2  34871  dihlsscpre  34879  dihvalcq2  34892  dihopelvalcpre  34893  dihord6apre  34901  dihord5b  34904  dihord5apre  34907  dihmeetlem1N  34935  dihglblem5apreN  34936  dihglblem2aN  34938  dihglblem2N  34939  dihmeetlem2N  34944  dihglbcpreN  34945  dihmeetbclemN  34949  dihmeetlem3N  34950  dihmeetlem4preN  34951  dihmeetlem6  34954  dihmeetlem7N  34955  dihjatc1  34956  dihjatc2N  34957  dihjatc3  34958  dihmeetlem9N  34960  dihmeetlem16N  34967  dihmeetlem19N  34970  dihmeetcl  34990  dihmeet2  34991  djhlj  35046  dihjatcclem1  35063  dihjatcclem2  35064  dihjatcclem4  35066