Theorem latmcl 15799

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

Syntax hints:   -> wi 4   /\ w3a 971   = wceq 1399   e. wcel 1826   ` cfv 5496  (class class class)co 6196   Basecbs 14634   joincjn 15690   meetcmee 15691   Latclat 15792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-lub 15721  df-glb 15722  df-join 15723  df-meet 15724  df-lat 15793

This theorem is referenced by:  latleeqm1  15826  latmlem1  15828  latmlem12  15830  latnlemlt  15831  latmidm  15833  latabs1  15834  latledi  15836  latmlej11  15837  mod1ile  15852  mod2ile  15853  latdisdlem  15936  oldmm1  35355  oldmj1  35359  latmrot  35370  latm4  35371  olm01  35374  omllaw4  35384  cmtcomlemN  35386  cmt2N  35388  cmtbr2N  35391  cmtbr3N  35392  cmtbr4N  35393  lecmtN  35394  omlfh1N  35396  omlfh3N  35397  meetat  35434  atnle  35455  atlatmstc  35457  hlrelat2  35540  cvrval5  35552  cvrexchlem  35556  cvrexch  35557  cvrat3  35579  cvrat4  35580  ps-2b  35619  2llnmat  35661  2atm  35664  llnmlplnN  35676  2lplnmN  35696  2llnmj  35697  2llnm2N  35705  2llnm4  35707  2lplnm2N  35758  2lplnmj  35759  dalemcea  35797  dalem16  35816  dalem21  35831  dalem54  35863  dalem55  35864  2lnat  35921  2atm2atN  35922  cdlema1N  35928  hlmod1i  35993  atmod1i1m  35995  atmod2i1  35998  atmod2i2  35999  llnmod2i2  36000  atmod4i1  36003  atmod4i2  36004  llnexchb2lem  36005  dalawlem1  36008  dalawlem2  36009  dalawlem3  36010  dalawlem4  36011  dalawlem5  36012  dalawlem6  36013  dalawlem7  36014  dalawlem8  36015  dalawlem9  36016  dalawlem11  36018  dalawlem12  36019  pmapj2N  36066  psubclinN  36085  poml4N  36090  pl42lem1N  36116  pl42lem2N  36117  pl42N  36120  lhpmcvr3  36162  lhpmcvr4N  36163  lhpmcvr5N  36164  lhpmcvr6N  36165  lhpelim  36174  lhpmod2i2  36175  lhpmod6i1  36176  lhprelat3N  36177  lautm  36231  trlval2  36301  trlcl  36302  trlval3  36325  cdlemc1  36329  cdlemc2  36330  cdlemc4  36332  cdlemc5  36333  cdlemc6  36334  cdlemd2  36337  cdleme0aa  36348  cdleme1b  36364  cdleme1  36365  cdleme2  36366  cdleme3b  36367  cdleme3h  36373  cdleme4a  36377  cdleme5  36378  cdleme7e  36385  cdleme7ga  36386  cdleme9b  36390  cdleme11g  36403  cdleme15d  36415  cdleme15  36416  cdleme16b  36417  cdleme16e  36420  cdleme16f  36421  cdleme22gb  36432  cdlemedb  36435  cdleme20j  36457  cdleme22cN  36481  cdleme22e  36483  cdleme22eALTN  36484  cdleme22f  36485  cdleme23a  36488  cdleme23b  36489  cdleme23c  36490  cdleme28a  36509  cdleme28b  36510  cdleme29ex  36513  cdleme30a  36517  cdlemefr29exN  36541  cdleme32c  36582  cdleme32e  36584  cdleme35b  36589  cdleme35c  36590  cdleme35d  36591  cdleme42c  36611  cdleme42h  36621  cdleme42i  36622  cdleme48bw  36641  cdlemg7fvbwN  36746  cdlemg10bALTN  36775  cdlemg10  36780  cdlemg11b  36781  cdlemg12f  36787  cdlemg12g  36788  cdlemg17a  36800  trlcolem  36865  cdlemkvcl  36981  cdlemk5u  37000  cdlemk37  37053  cdlemk52  37093  dia2dimlem2  37205  docaclN  37264  doca2N  37266  djajN  37277  cdlemn10  37346  dihjustlem  37356  dihord1  37358  dihord2a  37359  dihord2b  37360  dihord2cN  37361  dihord11b  37362  dihord11c  37364  dihord2pre  37365  dihord2pre2  37366  dihlsscpre  37374  dihvalcq2  37387  dihopelvalcpre  37388  dihord6apre  37396  dihord5b  37399  dihord5apre  37402  dihmeetlem1N  37430  dihglblem5apreN  37431  dihglblem2aN  37433  dihglblem2N  37434  dihmeetlem2N  37439  dihglbcpreN  37440  dihmeetbclemN  37444  dihmeetlem3N  37445  dihmeetlem4preN  37446  dihmeetlem6  37449  dihmeetlem7N  37450  dihjatc1  37451  dihjatc2N  37452  dihjatc3  37453  dihmeetlem9N  37455  dihmeetlem16N  37462  dihmeetlem19N  37465  dihmeetcl  37485  dihmeet2  37486  djhlj  37541  dihjatcclem1  37558  dihjatcclem2  37559  dihjatcclem4  37561