Theorem latmcl 18534

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  joincjn 18405  meetcmee 18406  Latclat 18525

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 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-lub 18438  df-glb 18439  df-join 18440  df-meet 18441  df-lat 18526

This theorem is used by:  latleeqm1  18561  latmlem1  18563  latmlem12  18565  latnlemlt  18566  latmidm  18568  latabs1  18569  latledi  18571  latmlej11  18572  mod1ile  18587  mod2ile  18588  latdisdlem  18590  oldmm1  40098  oldmj1  40102  latmrot  40113  latm4  40114  olm01  40117  omllaw4  40127  cmtcomlemN  40129  cmt2N  40131  cmtbr2N  40134  cmtbr3N  40135  cmtbr4N  40136  lecmtN  40137  omlfh1N  40139  omlfh3N  40140  meetat  40177  atnle  40198  atlatmstc  40200  hlrelat2  40284  cvrval5  40296  cvrexchlem  40300  cvrexch  40301  cvrat3  40323  cvrat4  40324  ps-2b  40363  2llnmat  40405  2atm  40408  llnmlplnN  40420  2lplnmN  40440  2llnmj  40441  2llnm2N  40449  2llnm4  40451  2lplnm2N  40502  2lplnmj  40503  dalemcea  40541  dalem16  40560  dalem21  40575  dalem54  40607  dalem55  40608  2lnat  40665  2atm2atN  40666  cdlema1N  40672  hlmod1i  40737  atmod1i1m  40739  atmod2i1  40742  atmod2i2  40743  llnmod2i2  40744  atmod4i1  40747  atmod4i2  40748  llnexchb2lem  40749  dalawlem1  40752  dalawlem2  40753  dalawlem3  40754  dalawlem4  40755  dalawlem5  40756  dalawlem6  40757  dalawlem7  40758  dalawlem8  40759  dalawlem9  40760  dalawlem11  40762  dalawlem12  40763  pmapj2N  40810  psubclinN  40829  poml4N  40834  pl42lem1N  40860  pl42lem2N  40861  pl42N  40864  lhpmcvr3  40906  lhpmcvr4N  40907  lhpmcvr5N  40908  lhpmcvr6N  40909  lhpelim  40918  lhpmod2i2  40919  lhpmod6i1  40920  lhprelat3N  40921  lautm  40975  trlval2  41044  trlcl  41045  trlval3  41068  cdlemc1  41072  cdlemc2  41073  cdlemc4  41075  cdlemc5  41076  cdlemc6  41077  cdlemd2  41080  cdleme0aa  41091  cdleme1b  41107  cdleme1  41108  cdleme2  41109  cdleme3b  41110  cdleme3h  41116  cdleme4a  41120  cdleme5  41121  cdleme7e  41128  cdleme7ga  41129  cdleme9b  41133  cdleme11g  41146  cdleme15d  41158  cdleme15  41159  cdleme16b  41160  cdleme16e  41163  cdleme16f  41164  cdleme22gb  41175  cdlemedb  41178  cdleme20j  41199  cdleme22cN  41223  cdleme22e  41225  cdleme22eALTN  41226  cdleme22f  41227  cdleme23a  41230  cdleme23b  41231  cdleme23c  41232  cdleme28a  41251  cdleme28b  41252  cdleme29ex  41255  cdleme30a  41259  cdlemefr29exN  41283  cdleme32c  41324  cdleme32e  41326  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme42c  41353  cdleme42h  41363  cdleme42i  41364  cdleme48bw  41383  cdlemg7fvbwN  41488  cdlemg10bALTN  41517  cdlemg10  41522  cdlemg11b  41523  cdlemg12f  41529  cdlemg12g  41530  cdlemg17a  41542  trlcolem  41607  cdlemkvcl  41723  cdlemk5u  41742  cdlemk37  41795  cdlemk52  41835  dia2dimlem2  41946  docaclN  42005  doca2N  42007  djajN  42018  cdlemn10  42087  dihjustlem  42097  dihord1  42099  dihord2a  42100  dihord2b  42101  dihord2cN  42102  dihord11b  42103  dihord11c  42105  dihord2pre  42106  dihord2pre2  42107  dihlsscpre  42115  dihvalcq2  42128  dihopelvalcpre  42129  dihord6apre  42137  dihord5b  42140  dihord5apre  42143  dihmeetlem1N  42171  dihglblem5apreN  42172  dihglblem2aN  42174  dihglblem2N  42175  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetbclemN  42185  dihmeetlem3N  42186  dihmeetlem4preN  42187  dihmeetlem6  42190  dihmeetlem7N  42191  dihjatc1  42192  dihjatc2N  42193  dihjatc3  42194  dihmeetlem9N  42196  dihmeetlem16N  42203  dihmeetlem19N  42206  dihmeetcl  42226  dihmeet2  42227  djhlj  42282  dihjatcclem1  42299  dihjatcclem2  42300  dihjatcclem4  42302