Theorem latmcl 18529

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 2760	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
3		latmcl.m	. . 3 ⊢ ∧ = (meet‘𝐾)
4	1, 2, 3	latlem 18526	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 501	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7414  Basecbs 17302  joincjn 18400  meetcmee 18401  Latclat 18520

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 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-lub 18433  df-glb 18434  df-join 18435  df-meet 18436  df-lat 18521

This theorem is used by:  latleeqm1  18556  latmlem1  18558  latmlem12  18560  latnlemlt  18561  latmidm  18563  latabs1  18564  latledi  18566  latmlej11  18567  mod1ile  18582  mod2ile  18583  latdisdlem  18585  oldmm1  40091  oldmj1  40095  latmrot  40106  latm4  40107  olm01  40110  omllaw4  40120  cmtcomlemN  40122  cmt2N  40124  cmtbr2N  40127  cmtbr3N  40128  cmtbr4N  40129  lecmtN  40130  omlfh1N  40132  omlfh3N  40133  meetat  40170  atnle  40191  atlatmstc  40193  hlrelat2  40277  cvrval5  40289  cvrexchlem  40293  cvrexch  40294  cvrat3  40316  cvrat4  40317  ps-2b  40356  2llnmat  40398  2atm  40401  llnmlplnN  40413  2lplnmN  40433  2llnmj  40434  2llnm2N  40442  2llnm4  40444  2lplnm2N  40495  2lplnmj  40496  dalemcea  40534  dalem16  40553  dalem21  40568  dalem54  40600  dalem55  40601  2lnat  40658  2atm2atN  40659  cdlema1N  40665  hlmod1i  40730  atmod1i1m  40732  atmod2i1  40735  atmod2i2  40736  llnmod2i2  40737  atmod4i1  40740  atmod4i2  40741  llnexchb2lem  40742  dalawlem1  40745  dalawlem2  40746  dalawlem3  40747  dalawlem4  40748  dalawlem5  40749  dalawlem6  40750  dalawlem7  40751  dalawlem8  40752  dalawlem9  40753  dalawlem11  40755  dalawlem12  40756  pmapj2N  40803  psubclinN  40822  poml4N  40827  pl42lem1N  40853  pl42lem2N  40854  pl42N  40857  lhpmcvr3  40899  lhpmcvr4N  40900  lhpmcvr5N  40901  lhpmcvr6N  40902  lhpelim  40911  lhpmod2i2  40912  lhpmod6i1  40913  lhprelat3N  40914  lautm  40968  trlval2  41037  trlcl  41038  trlval3  41061  cdlemc1  41065  cdlemc2  41066  cdlemc4  41068  cdlemc5  41069  cdlemc6  41070  cdlemd2  41073  cdleme0aa  41084  cdleme1b  41100  cdleme1  41101  cdleme2  41102  cdleme3b  41103  cdleme3h  41109  cdleme4a  41113  cdleme5  41114  cdleme7e  41121  cdleme7ga  41122  cdleme9b  41126  cdleme11g  41139  cdleme15d  41151  cdleme15  41152  cdleme16b  41153  cdleme16e  41156  cdleme16f  41157  cdleme22gb  41168  cdlemedb  41171  cdleme20j  41192  cdleme22cN  41216  cdleme22e  41218  cdleme22eALTN  41219  cdleme22f  41220  cdleme23a  41223  cdleme23b  41224  cdleme23c  41225  cdleme28a  41244  cdleme28b  41245  cdleme29ex  41248  cdleme30a  41252  cdlemefr29exN  41276  cdleme32c  41317  cdleme32e  41319  cdleme35b  41324  cdleme35c  41325  cdleme35d  41326  cdleme42c  41346  cdleme42h  41356  cdleme42i  41357  cdleme48bw  41376  cdlemg7fvbwN  41481  cdlemg10bALTN  41510  cdlemg10  41515  cdlemg11b  41516  cdlemg12f  41522  cdlemg12g  41523  cdlemg17a  41535  trlcolem  41600  cdlemkvcl  41716  cdlemk5u  41735  cdlemk37  41788  cdlemk52  41828  dia2dimlem2  41939  docaclN  41998  doca2N  42000  djajN  42011  cdlemn10  42080  dihjustlem  42090  dihord1  42092  dihord2a  42093  dihord2b  42094  dihord2cN  42095  dihord11b  42096  dihord11c  42098  dihord2pre  42099  dihord2pre2  42100  dihlsscpre  42108  dihvalcq2  42121  dihopelvalcpre  42122  dihord6apre  42130  dihord5b  42133  dihord5apre  42136  dihmeetlem1N  42164  dihglblem5apreN  42165  dihglblem2aN  42167  dihglblem2N  42168  dihmeetlem2N  42173  dihglbcpreN  42174  dihmeetbclemN  42178  dihmeetlem3N  42179  dihmeetlem4preN  42180  dihmeetlem6  42183  dihmeetlem7N  42184  dihjatc1  42185  dihjatc2N  42186  dihjatc3  42187  dihmeetlem9N  42189  dihmeetlem16N  42196  dihmeetlem19N  42199  dihmeetcl  42219  dihmeet2  42220  djhlj  42275  dihjatcclem1  42292  dihjatcclem2  42293  dihjatcclem4  42295