Theorem latmcl 18485

Description: Closure of meet operation in a lattice. (incom 4209 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 2737	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
3		latmcl.m	. . 3 ⊢ ∧ = (meet‘𝐾)
4	1, 2, 3	latlem 18482	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 495	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  joincjn 18357  meetcmee 18358  Latclat 18476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-lub 18391  df-glb 18392  df-join 18393  df-meet 18394  df-lat 18477

This theorem is referenced by:  latleeqm1  18512  latmlem1  18514  latmlem12  18516  latnlemlt  18517  latmidm  18519  latabs1  18520  latledi  18522  latmlej11  18523  mod1ile  18538  mod2ile  18539  latdisdlem  18541  oldmm1  39218  oldmj1  39222  latmrot  39233  latm4  39234  olm01  39237  omllaw4  39247  cmtcomlemN  39249  cmt2N  39251  cmtbr2N  39254  cmtbr3N  39255  cmtbr4N  39256  lecmtN  39257  omlfh1N  39259  omlfh3N  39260  meetat  39297  atnle  39318  atlatmstc  39320  hlrelat2  39405  cvrval5  39417  cvrexchlem  39421  cvrexch  39422  cvrat3  39444  cvrat4  39445  ps-2b  39484  2llnmat  39526  2atm  39529  llnmlplnN  39541  2lplnmN  39561  2llnmj  39562  2llnm2N  39570  2llnm4  39572  2lplnm2N  39623  2lplnmj  39624  dalemcea  39662  dalem16  39681  dalem21  39696  dalem54  39728  dalem55  39729  2lnat  39786  2atm2atN  39787  cdlema1N  39793  hlmod1i  39858  atmod1i1m  39860  atmod2i1  39863  atmod2i2  39864  llnmod2i2  39865  atmod4i1  39868  atmod4i2  39869  llnexchb2lem  39870  dalawlem1  39873  dalawlem2  39874  dalawlem3  39875  dalawlem4  39876  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  pmapj2N  39931  psubclinN  39950  poml4N  39955  pl42lem1N  39981  pl42lem2N  39982  pl42N  39985  lhpmcvr3  40027  lhpmcvr4N  40028  lhpmcvr5N  40029  lhpmcvr6N  40030  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  lhprelat3N  40042  lautm  40096  trlval2  40165  trlcl  40166  trlval3  40189  cdlemc1  40193  cdlemc2  40194  cdlemc4  40196  cdlemc5  40197  cdlemc6  40198  cdlemd2  40201  cdleme0aa  40212  cdleme1b  40228  cdleme1  40229  cdleme2  40230  cdleme3b  40231  cdleme3h  40237  cdleme4a  40241  cdleme5  40242  cdleme7e  40249  cdleme7ga  40250  cdleme9b  40254  cdleme11g  40267  cdleme15d  40279  cdleme15  40280  cdleme16b  40281  cdleme16e  40284  cdleme16f  40285  cdleme22gb  40296  cdlemedb  40299  cdleme20j  40320  cdleme22cN  40344  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme23a  40351  cdleme23b  40352  cdleme23c  40353  cdleme28a  40372  cdleme28b  40373  cdleme29ex  40376  cdleme30a  40380  cdlemefr29exN  40404  cdleme32c  40445  cdleme32e  40447  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme42c  40474  cdleme42h  40484  cdleme42i  40485  cdleme48bw  40504  cdlemg7fvbwN  40609  cdlemg10bALTN  40638  cdlemg10  40643  cdlemg11b  40644  cdlemg12f  40650  cdlemg12g  40651  cdlemg17a  40663  trlcolem  40728  cdlemkvcl  40844  cdlemk5u  40863  cdlemk37  40916  cdlemk52  40956  dia2dimlem2  41067  docaclN  41126  doca2N  41128  djajN  41139  cdlemn10  41208  dihjustlem  41218  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord2cN  41223  dihord11b  41224  dihord11c  41226  dihord2pre  41227  dihord2pre2  41228  dihlsscpre  41236  dihvalcq2  41249  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem2aN  41295  dihglblem2N  41296  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetbclemN  41306  dihmeetlem3N  41307  dihmeetlem4preN  41308  dihmeetlem6  41311  dihmeetlem7N  41312  dihjatc1  41313  dihjatc2N  41314  dihjatc3  41315  dihmeetlem9N  41317  dihmeetlem16N  41324  dihmeetlem19N  41327  dihmeetcl  41347  dihmeet2  41348  djhlj  41403  dihjatcclem1  41420  dihjatcclem2  41421  dihjatcclem4  41423