Theorem latmcl 14435

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

Syntax hints:   -> wi 4   /\ w3a 936   = wceq 1649   e. wcel 1721   ` cfv 5413  (class class class)co 6040   Basecbs 13424   joincjn 14356   meetcmee 14357   Latclat 14429

This theorem is referenced by:  latmcom  14459  latmle1  14460  latmle2  14461  latlem12  14462  latleeqm1  14463  latmlem1  14465  latmlem12  14467  latnlemlt  14468  latmidm  14470  latabs1  14471  latledi  14473  latmlej11  14474  mod1ile  14489  mod2ile  14490  latdisdlem  14570  oldmm1  29700  oldmj1  29704  latmrot  29715  latm4  29716  olm01  29719  omllaw4  29729  cmtcomlemN  29731  cmt2N  29733  cmtbr2N  29736  cmtbr3N  29737  cmtbr4N  29738  lecmtN  29739  omlfh1N  29741  omlfh3N  29742  meetat  29779  atnle  29800  atlatmstc  29802  hlrelat2  29885  cvrval5  29897  cvrexchlem  29901  cvrexch  29902  cvrat3  29924  cvrat4  29925  ps-2b  29964  2llnmat  30006  2atm  30009  llnmlplnN  30021  2lplnmN  30041  2llnmj  30042  2llnm2N  30050  2llnm4  30052  2lplnm2N  30103  2lplnmj  30104  dalemcea  30142  dalem16  30161  dalem21  30176  dalem54  30208  dalem55  30209  2lnat  30266  2atm2atN  30267  cdlema1N  30273  hlmod1i  30338  atmod1i1m  30340  atmod2i1  30343  atmod2i2  30344  llnmod2i2  30345  atmod4i1  30348  atmod4i2  30349  llnexchb2lem  30350  dalawlem1  30353  dalawlem2  30354  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  pmapj2N  30411  psubclinN  30430  poml4N  30435  pl42lem1N  30461  pl42lem2N  30462  pl42N  30465  lhpmcvr3  30507  lhpmcvr4N  30508  lhpmcvr5N  30509  lhpmcvr6N  30510  lhpelim  30519  lhpmod2i2  30520  lhpmod6i1  30521  lhprelat3N  30522  lautm  30576  trlval2  30645  trlcl  30646  trlval3  30669  cdlemc1  30673  cdlemc2  30674  cdlemc4  30676  cdlemc5  30677  cdlemc6  30678  cdlemd2  30681  cdleme0aa  30692  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3b  30711  cdleme3h  30717  cdleme4a  30721  cdleme5  30722  cdleme7e  30729  cdleme7ga  30730  cdleme9b  30734  cdleme11g  30747  cdleme15d  30759  cdleme15  30760  cdleme16b  30761  cdleme16e  30764  cdleme16f  30765  cdleme22gb  30776  cdlemedb  30779  cdleme20j  30800  cdleme22cN  30824  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f  30828  cdleme23a  30831  cdleme23b  30832  cdleme23c  30833  cdleme28a  30852  cdleme28b  30853  cdleme29ex  30856  cdleme30a  30860  cdlemefr29exN  30884  cdleme32c  30925  cdleme32e  30927  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme42c  30954  cdleme42h  30964  cdleme42i  30965  cdleme48bw  30984  cdlemg7fvbwN  31089  cdlemg10bALTN  31118  cdlemg10  31123  cdlemg11b  31124  cdlemg12f  31130  cdlemg12g  31131  cdlemg17a  31143  trlcolem  31208  cdlemkvcl  31324  cdlemk5u  31343  cdlemk37  31396  cdlemk52  31436  dia2dimlem2  31548  docaclN  31607  doca2N  31609  djajN  31620  cdlemn10  31689  dihjustlem  31699  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord2cN  31704  dihord11b  31705  dihord11c  31707  dihord2pre  31708  dihord2pre2  31709  dihlsscpre  31717  dihvalcq2  31730  dihopelvalcpre  31731  dihord6apre  31739  dihord5b  31742  dihord5apre  31745  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem2aN  31776  dihglblem2N  31777  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetbclemN  31787  dihmeetlem3N  31788  dihmeetlem4preN  31789  dihmeetlem6  31792  dihmeetlem7N  31793  dihjatc1  31794  dihjatc2N  31795  dihjatc3  31796  dihmeetlem9N  31798  dihmeetlem16N  31805  dihmeetlem19N  31808  dihmeetcl  31828  dihmeet2  31829  djhlj  31884  dihjatcclem1  31901  dihjatcclem2  31902  dihjatcclem4  31904

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-lat 14430