Theorem latmcl 15539

Description: Closure of meet operation in a lattice. (incom 3691 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 2467	. . 3 |- ( join ` K ) = ( join ` K )
3		latmcl.m	. . 3 |- ./\ = ( meet ` K )
4	1, 2, 3	latlem 15536	. 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 973   = wceq 1379   e. wcel 1767   ` cfv 5588  (class class class)co 6284   Basecbs 14490   joincjn 15431   meetcmee 15432   Latclat 15532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-lub 15461  df-glb 15462  df-join 15463  df-meet 15464  df-lat 15533

This theorem is referenced by:  latleeqm1  15566  latmlem1  15568  latmlem12  15570  latnlemlt  15571  latmidm  15573  latabs1  15574  latledi  15576  latmlej11  15577  mod1ile  15592  mod2ile  15593  latdisdlem  15676  oldmm1  34032  oldmj1  34036  latmrot  34047  latm4  34048  olm01  34051  omllaw4  34061  cmtcomlemN  34063  cmt2N  34065  cmtbr2N  34068  cmtbr3N  34069  cmtbr4N  34070  lecmtN  34071  omlfh1N  34073  omlfh3N  34074  meetat  34111  atnle  34132  atlatmstc  34134  hlrelat2  34217  cvrval5  34229  cvrexchlem  34233  cvrexch  34234  cvrat3  34256  cvrat4  34257  ps-2b  34296  2llnmat  34338  2atm  34341  llnmlplnN  34353  2lplnmN  34373  2llnmj  34374  2llnm2N  34382  2llnm4  34384  2lplnm2N  34435  2lplnmj  34436  dalemcea  34474  dalem16  34493  dalem21  34508  dalem54  34540  dalem55  34541  2lnat  34598  2atm2atN  34599  cdlema1N  34605  hlmod1i  34670  atmod1i1m  34672  atmod2i1  34675  atmod2i2  34676  llnmod2i2  34677  atmod4i1  34680  atmod4i2  34681  llnexchb2lem  34682  dalawlem1  34685  dalawlem2  34686  dalawlem3  34687  dalawlem4  34688  dalawlem5  34689  dalawlem6  34690  dalawlem7  34691  dalawlem8  34692  dalawlem9  34693  dalawlem11  34695  dalawlem12  34696  pmapj2N  34743  psubclinN  34762  poml4N  34767  pl42lem1N  34793  pl42lem2N  34794  pl42N  34797  lhpmcvr3  34839  lhpmcvr4N  34840  lhpmcvr5N  34841  lhpmcvr6N  34842  lhpelim  34851  lhpmod2i2  34852  lhpmod6i1  34853  lhprelat3N  34854  lautm  34908  trlval2  34977  trlcl  34978  trlval3  35001  cdlemc1  35005  cdlemc2  35006  cdlemc4  35008  cdlemc5  35009  cdlemc6  35010  cdlemd2  35013  cdleme0aa  35024  cdleme1b  35040  cdleme1  35041  cdleme2  35042  cdleme3b  35043  cdleme3h  35049  cdleme4a  35053  cdleme5  35054  cdleme7e  35061  cdleme7ga  35062  cdleme9b  35066  cdleme11g  35079  cdleme15d  35091  cdleme15  35092  cdleme16b  35093  cdleme16e  35096  cdleme16f  35097  cdleme22gb  35108  cdlemedb  35111  cdleme20j  35132  cdleme22cN  35156  cdleme22e  35158  cdleme22eALTN  35159  cdleme22f  35160  cdleme23a  35163  cdleme23b  35164  cdleme23c  35165  cdleme28a  35184  cdleme28b  35185  cdleme29ex  35188  cdleme30a  35192  cdlemefr29exN  35216  cdleme32c  35257  cdleme32e  35259  cdleme35b  35264  cdleme35c  35265  cdleme35d  35266  cdleme42c  35286  cdleme42h  35296  cdleme42i  35297  cdleme48bw  35316  cdlemg7fvbwN  35421  cdlemg10bALTN  35450  cdlemg10  35455  cdlemg11b  35456  cdlemg12f  35462  cdlemg12g  35463  cdlemg17a  35475  trlcolem  35540  cdlemkvcl  35656  cdlemk5u  35675  cdlemk37  35728  cdlemk52  35768  dia2dimlem2  35880  docaclN  35939  doca2N  35941  djajN  35952  cdlemn10  36021  dihjustlem  36031  dihord1  36033  dihord2a  36034  dihord2b  36035  dihord2cN  36036  dihord11b  36037  dihord11c  36039  dihord2pre  36040  dihord2pre2  36041  dihlsscpre  36049  dihvalcq2  36062  dihopelvalcpre  36063  dihord6apre  36071  dihord5b  36074  dihord5apre  36077  dihmeetlem1N  36105  dihglblem5apreN  36106  dihglblem2aN  36108  dihglblem2N  36109  dihmeetlem2N  36114  dihglbcpreN  36115  dihmeetbclemN  36119  dihmeetlem3N  36120  dihmeetlem4preN  36121  dihmeetlem6  36124  dihmeetlem7N  36125  dihjatc1  36126  dihjatc2N  36127  dihjatc3  36128  dihmeetlem9N  36130  dihmeetlem16N  36137  dihmeetlem19N  36140  dihmeetcl  36160  dihmeet2  36161  djhlj  36216  dihjatcclem1  36233  dihjatcclem2  36234  dihjatcclem4  36236