Theorem latmcl 18614

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  joincjn 18485  meetcmee 18486  Latclat 18605

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-lub 18518  df-glb 18519  df-join 18520  df-meet 18521  df-lat 18606

This theorem is used by:  latleeqm1  18641  latmlem1  18643  latmlem12  18645  latnlemlt  18646  latmidm  18648  latabs1  18649  latledi  18651  latmlej11  18652  mod1ile  18667  mod2ile  18668  latdisdlem  18670  oldmm1  40274  oldmj1  40278  latmrot  40289  latm4  40290  olm01  40293  omllaw4  40303  cmtcomlemN  40305  cmt2N  40307  cmtbr2N  40310  cmtbr3N  40311  cmtbr4N  40312  lecmtN  40313  omlfh1N  40315  omlfh3N  40316  meetat  40353  atnle  40374  atlatmstc  40376  hlrelat2  40460  cvrval5  40472  cvrexchlem  40476  cvrexch  40477  cvrat3  40499  cvrat4  40500  ps-2b  40539  2llnmat  40581  2atm  40584  llnmlplnN  40596  2lplnmN  40616  2llnmj  40617  2llnm2N  40625  2llnm4  40627  2lplnm2N  40678  2lplnmj  40679  dalemcea  40717  dalem16  40736  dalem21  40751  dalem54  40783  dalem55  40784  2lnat  40841  2atm2atN  40842  cdlema1N  40848  hlmod1i  40913  atmod1i1m  40915  atmod2i1  40918  atmod2i2  40919  llnmod2i2  40920  atmod4i1  40923  atmod4i2  40924  llnexchb2lem  40925  dalawlem1  40928  dalawlem2  40929  dalawlem3  40930  dalawlem4  40931  dalawlem5  40932  dalawlem6  40933  dalawlem7  40934  dalawlem8  40935  dalawlem9  40936  dalawlem11  40938  dalawlem12  40939  pmapj2N  40986  psubclinN  41005  poml4N  41010  pl42lem1N  41036  pl42lem2N  41037  pl42N  41040  lhpmcvr3  41082  lhpmcvr4N  41083  lhpmcvr5N  41084  lhpmcvr6N  41085  lhpelim  41094  lhpmod2i2  41095  lhpmod6i1  41096  lhprelat3N  41097  lautm  41151  trlval2  41220  trlcl  41221  trlval3  41244  cdlemc1  41248  cdlemc2  41249  cdlemc4  41251  cdlemc5  41252  cdlemc6  41253  cdlemd2  41256  cdleme0aa  41267  cdleme1b  41283  cdleme1  41284  cdleme2  41285  cdleme3b  41286  cdleme3h  41292  cdleme4a  41296  cdleme5  41297  cdleme7e  41304  cdleme7ga  41305  cdleme9b  41309  cdleme11g  41322  cdleme15d  41334  cdleme15  41335  cdleme16b  41336  cdleme16e  41339  cdleme16f  41340  cdleme22gb  41351  cdlemedb  41354  cdleme20j  41375  cdleme22cN  41399  cdleme22e  41401  cdleme22eALTN  41402  cdleme22f  41403  cdleme23a  41406  cdleme23b  41407  cdleme23c  41408  cdleme28a  41427  cdleme28b  41428  cdleme29ex  41431  cdleme30a  41435  cdlemefr29exN  41459  cdleme32c  41500  cdleme32e  41502  cdleme35b  41507  cdleme35c  41508  cdleme35d  41509  cdleme42c  41529  cdleme42h  41539  cdleme42i  41540  cdleme48bw  41559  cdlemg7fvbwN  41664  cdlemg10bALTN  41693  cdlemg10  41698  cdlemg11b  41699  cdlemg12f  41705  cdlemg12g  41706  cdlemg17a  41718  trlcolem  41783  cdlemkvcl  41899  cdlemk5u  41918  cdlemk37  41971  cdlemk52  42011  dia2dimlem2  42122  docaclN  42181  doca2N  42183  djajN  42194  cdlemn10  42263  dihjustlem  42273  dihord1  42275  dihord2a  42276  dihord2b  42277  dihord2cN  42278  dihord11b  42279  dihord11c  42281  dihord2pre  42282  dihord2pre2  42283  dihlsscpre  42291  dihvalcq2  42304  dihopelvalcpre  42305  dihord6apre  42313  dihord5b  42316  dihord5apre  42319  dihmeetlem1N  42347  dihglblem5apreN  42348  dihglblem2aN  42350  dihglblem2N  42351  dihmeetlem2N  42356  dihglbcpreN  42357  dihmeetbclemN  42361  dihmeetlem3N  42362  dihmeetlem4preN  42363  dihmeetlem6  42366  dihmeetlem7N  42367  dihjatc1  42368  dihjatc2N  42369  dihjatc3  42370  dihmeetlem9N  42372  dihmeetlem16N  42379  dihmeetlem19N  42382  dihmeetcl  42402  dihmeet2  42403  djhlj  42458  dihjatcclem1  42475  dihjatcclem2  42476  dihjatcclem4  42478