Theorem latmcl 17656

Description: Closure of meet operation in a lattice. (incom 4178 analog.) (Contributed by NM, 14-Sep-2011.)

Hypotheses

Ref	Expression
latmcl.b	⊢ 𝐵 = (Base‘𝐾)
latmcl.m	⊢ ∧ = (meet‘𝐾)

Assertion

Ref	Expression
latmcl	⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Proof of Theorem latmcl

Step	Hyp	Ref	Expression
1		latmcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		eqid 2821	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
3		latmcl.m	. . 3 ⊢ ∧ = (meet‘𝐾)
4	1, 2, 3	latlem 17653	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 498	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ‘cfv 6350  (class class class)co 7150  Basecbs 16477  joincjn 17548  meetcmee 17549  Latclat 17649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-lub 17578  df-glb 17579  df-join 17580  df-meet 17581  df-lat 17650

This theorem is referenced by:  latleeqm1  17683  latmlem1  17685  latmlem12  17687  latnlemlt  17688  latmidm  17690  latabs1  17691  latledi  17693  latmlej11  17694  mod1ile  17709  mod2ile  17710  latdisdlem  17793  oldmm1  36347  oldmj1  36351  latmrot  36362  latm4  36363  olm01  36366  omllaw4  36376  cmtcomlemN  36378  cmt2N  36380  cmtbr2N  36383  cmtbr3N  36384  cmtbr4N  36385  lecmtN  36386  omlfh1N  36388  omlfh3N  36389  meetat  36426  atnle  36447  atlatmstc  36449  hlrelat2  36533  cvrval5  36545  cvrexchlem  36549  cvrexch  36550  cvrat3  36572  cvrat4  36573  ps-2b  36612  2llnmat  36654  2atm  36657  llnmlplnN  36669  2lplnmN  36689  2llnmj  36690  2llnm2N  36698  2llnm4  36700  2lplnm2N  36751  2lplnmj  36752  dalemcea  36790  dalem16  36809  dalem21  36824  dalem54  36856  dalem55  36857  2lnat  36914  2atm2atN  36915  cdlema1N  36921  hlmod1i  36986  atmod1i1m  36988  atmod2i1  36991  atmod2i2  36992  llnmod2i2  36993  atmod4i1  36996  atmod4i2  36997  llnexchb2lem  36998  dalawlem1  37001  dalawlem2  37002  dalawlem3  37003  dalawlem4  37004  dalawlem5  37005  dalawlem6  37006  dalawlem7  37007  dalawlem8  37008  dalawlem9  37009  dalawlem11  37011  dalawlem12  37012  pmapj2N  37059  psubclinN  37078  poml4N  37083  pl42lem1N  37109  pl42lem2N  37110  pl42N  37113  lhpmcvr3  37155  lhpmcvr4N  37156  lhpmcvr5N  37157  lhpmcvr6N  37158  lhpelim  37167  lhpmod2i2  37168  lhpmod6i1  37169  lhprelat3N  37170  lautm  37224  trlval2  37293  trlcl  37294  trlval3  37317  cdlemc1  37321  cdlemc2  37322  cdlemc4  37324  cdlemc5  37325  cdlemc6  37326  cdlemd2  37329  cdleme0aa  37340  cdleme1b  37356  cdleme1  37357  cdleme2  37358  cdleme3b  37359  cdleme3h  37365  cdleme4a  37369  cdleme5  37370  cdleme7e  37377  cdleme7ga  37378  cdleme9b  37382  cdleme11g  37395  cdleme15d  37407  cdleme15  37408  cdleme16b  37409  cdleme16e  37412  cdleme16f  37413  cdleme22gb  37424  cdlemedb  37427  cdleme20j  37448  cdleme22cN  37472  cdleme22e  37474  cdleme22eALTN  37475  cdleme22f  37476  cdleme23a  37479  cdleme23b  37480  cdleme23c  37481  cdleme28a  37500  cdleme28b  37501  cdleme29ex  37504  cdleme30a  37508  cdlemefr29exN  37532  cdleme32c  37573  cdleme32e  37575  cdleme35b  37580  cdleme35c  37581  cdleme35d  37582  cdleme42c  37602  cdleme42h  37612  cdleme42i  37613  cdleme48bw  37632  cdlemg7fvbwN  37737  cdlemg10bALTN  37766  cdlemg10  37771  cdlemg11b  37772  cdlemg12f  37778  cdlemg12g  37779  cdlemg17a  37791  trlcolem  37856  cdlemkvcl  37972  cdlemk5u  37991  cdlemk37  38044  cdlemk52  38084  dia2dimlem2  38195  docaclN  38254  doca2N  38256  djajN  38267  cdlemn10  38336  dihjustlem  38346  dihord1  38348  dihord2a  38349  dihord2b  38350  dihord2cN  38351  dihord11b  38352  dihord11c  38354  dihord2pre  38355  dihord2pre2  38356  dihlsscpre  38364  dihvalcq2  38377  dihopelvalcpre  38378  dihord6apre  38386  dihord5b  38389  dihord5apre  38392  dihmeetlem1N  38420  dihglblem5apreN  38421  dihglblem2aN  38423  dihglblem2N  38424  dihmeetlem2N  38429  dihglbcpreN  38430  dihmeetbclemN  38434  dihmeetlem3N  38435  dihmeetlem4preN  38436  dihmeetlem6  38439  dihmeetlem7N  38440  dihjatc1  38441  dihjatc2N  38442  dihjatc3  38443  dihmeetlem9N  38445  dihmeetlem16N  38452  dihmeetlem19N  38455  dihmeetcl  38475  dihmeet2  38476  djhlj  38531  dihjatcclem1  38548  dihjatcclem2  38549  dihjatcclem4  38551