Theorem latmcl 18343

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ‘cfv 6501  (class class class)co 7362  Basecbs 17094  joincjn 18214  meetcmee 18215  Latclat 18334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-lub 18249  df-glb 18250  df-join 18251  df-meet 18252  df-lat 18335

This theorem is referenced by:  latleeqm1  18370  latmlem1  18372  latmlem12  18374  latnlemlt  18375  latmidm  18377  latabs1  18378  latledi  18380  latmlej11  18381  mod1ile  18396  mod2ile  18397  latdisdlem  18399  oldmm1  37752  oldmj1  37756  latmrot  37767  latm4  37768  olm01  37771  omllaw4  37781  cmtcomlemN  37783  cmt2N  37785  cmtbr2N  37788  cmtbr3N  37789  cmtbr4N  37790  lecmtN  37791  omlfh1N  37793  omlfh3N  37794  meetat  37831  atnle  37852  atlatmstc  37854  hlrelat2  37939  cvrval5  37951  cvrexchlem  37955  cvrexch  37956  cvrat3  37978  cvrat4  37979  ps-2b  38018  2llnmat  38060  2atm  38063  llnmlplnN  38075  2lplnmN  38095  2llnmj  38096  2llnm2N  38104  2llnm4  38106  2lplnm2N  38157  2lplnmj  38158  dalemcea  38196  dalem16  38215  dalem21  38230  dalem54  38262  dalem55  38263  2lnat  38320  2atm2atN  38321  cdlema1N  38327  hlmod1i  38392  atmod1i1m  38394  atmod2i1  38397  atmod2i2  38398  llnmod2i2  38399  atmod4i1  38402  atmod4i2  38403  llnexchb2lem  38404  dalawlem1  38407  dalawlem2  38408  dalawlem3  38409  dalawlem4  38410  dalawlem5  38411  dalawlem6  38412  dalawlem7  38413  dalawlem8  38414  dalawlem9  38415  dalawlem11  38417  dalawlem12  38418  pmapj2N  38465  psubclinN  38484  poml4N  38489  pl42lem1N  38515  pl42lem2N  38516  pl42N  38519  lhpmcvr3  38561  lhpmcvr4N  38562  lhpmcvr5N  38563  lhpmcvr6N  38564  lhpelim  38573  lhpmod2i2  38574  lhpmod6i1  38575  lhprelat3N  38576  lautm  38630  trlval2  38699  trlcl  38700  trlval3  38723  cdlemc1  38727  cdlemc2  38728  cdlemc4  38730  cdlemc5  38731  cdlemc6  38732  cdlemd2  38735  cdleme0aa  38746  cdleme1b  38762  cdleme1  38763  cdleme2  38764  cdleme3b  38765  cdleme3h  38771  cdleme4a  38775  cdleme5  38776  cdleme7e  38783  cdleme7ga  38784  cdleme9b  38788  cdleme11g  38801  cdleme15d  38813  cdleme15  38814  cdleme16b  38815  cdleme16e  38818  cdleme16f  38819  cdleme22gb  38830  cdlemedb  38833  cdleme20j  38854  cdleme22cN  38878  cdleme22e  38880  cdleme22eALTN  38881  cdleme22f  38882  cdleme23a  38885  cdleme23b  38886  cdleme23c  38887  cdleme28a  38906  cdleme28b  38907  cdleme29ex  38910  cdleme30a  38914  cdlemefr29exN  38938  cdleme32c  38979  cdleme32e  38981  cdleme35b  38986  cdleme35c  38987  cdleme35d  38988  cdleme42c  39008  cdleme42h  39018  cdleme42i  39019  cdleme48bw  39038  cdlemg7fvbwN  39143  cdlemg10bALTN  39172  cdlemg10  39177  cdlemg11b  39178  cdlemg12f  39184  cdlemg12g  39185  cdlemg17a  39197  trlcolem  39262  cdlemkvcl  39378  cdlemk5u  39397  cdlemk37  39450  cdlemk52  39490  dia2dimlem2  39601  docaclN  39660  doca2N  39662  djajN  39673  cdlemn10  39742  dihjustlem  39752  dihord1  39754  dihord2a  39755  dihord2b  39756  dihord2cN  39757  dihord11b  39758  dihord11c  39760  dihord2pre  39761  dihord2pre2  39762  dihlsscpre  39770  dihvalcq2  39783  dihopelvalcpre  39784  dihord6apre  39792  dihord5b  39795  dihord5apre  39798  dihmeetlem1N  39826  dihglblem5apreN  39827  dihglblem2aN  39829  dihglblem2N  39830  dihmeetlem2N  39835  dihglbcpreN  39836  dihmeetbclemN  39840  dihmeetlem3N  39841  dihmeetlem4preN  39842  dihmeetlem6  39845  dihmeetlem7N  39846  dihjatc1  39847  dihjatc2N  39848  dihjatc3  39849  dihmeetlem9N  39851  dihmeetlem16N  39858  dihmeetlem19N  39861  dihmeetcl  39881  dihmeet2  39882  djhlj  39937  dihjatcclem1  39954  dihjatcclem2  39955  dihjatcclem4  39957