MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latjcl Structured version   Visualization version   GIF version

Theorem latjcl 16972
Description: Closure of join operation in a lattice. (chjcom 28214 analog.) (Contributed by NM, 14-Sep-2011.)
Hypotheses
Ref Expression
latjcl.b 𝐵 = (Base‘𝐾)
latjcl.j = (join‘𝐾)
Assertion
Ref Expression
latjcl ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)

Proof of Theorem latjcl
StepHypRef Expression
1 latjcl.b . . 3 𝐵 = (Base‘𝐾)
2 latjcl.j . . 3 = (join‘𝐾)
3 eqid 2621 . . 3 (meet‘𝐾) = (meet‘𝐾)
41, 2, 3latlem 16970 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵))
54simpld 475 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1480  wcel 1987  cfv 5847  (class class class)co 6604  Basecbs 15781  joincjn 16865  meetcmee 16866  Latclat 16966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-lub 16895  df-glb 16896  df-join 16897  df-meet 16898  df-lat 16967
This theorem is referenced by:  latleeqj1  16984  latjlej1  16986  latjlej12  16988  latnlej2  16992  latjidm  16995  latnle  17006  latabs2  17009  latledi  17010  latmlej11  17011  latjass  17016  latj13  17019  latj31  17020  latj4  17022  mod1ile  17026  mod2ile  17027  lubun  17044  latdisdlem  17110  oldmm1  33984  olj01  33992  latmassOLD  33996  omllaw5N  34014  cmtcomlemN  34015  cmtbr2N  34020  cmtbr3N  34021  cmtbr4N  34022  lecmtN  34023  omlfh1N  34025  omlfh3N  34026  omlmod1i2N  34027  cvlexchb1  34097  cvlcvr1  34106  hlatjcl  34133  exatleN  34170  cvrval3  34179  cvrexchlem  34185  cvrexch  34186  cvratlem  34187  cvrat  34188  lnnat  34193  cvrat2  34195  atcvrj2b  34198  atltcvr  34201  atlelt  34204  2atlt  34205  atexchcvrN  34206  cvrat3  34208  cvrat4  34209  2atjm  34211  4noncolr3  34219  athgt  34222  3dim0  34223  3dimlem4a  34229  1cvratex  34239  1cvrjat  34241  1cvrat  34242  ps-2  34244  3atlem1  34249  3atlem2  34250  3at  34256  2atm  34293  lplni2  34303  lplnle  34306  2llnmj  34326  2atmat  34327  lplnexllnN  34330  2llnjaN  34332  lvoli3  34343  islvol5  34345  lvoli2  34347  lvolnle3at  34348  3atnelvolN  34352  islvol2aN  34358  4atlem3  34362  4atlem4d  34368  4atlem9  34369  4atlem10a  34370  4atlem10  34372  4atlem11a  34373  4atlem11b  34374  4atlem11  34375  4atlem12a  34376  4atlem12b  34377  4atlem12  34378  4at  34379  lplncvrlvol2  34381  2lplnja  34385  2lplnmj  34388  dalem5  34433  dalem8  34436  dalem-cly  34437  dalem38  34476  dalem39  34477  dalem44  34482  dalem54  34492  linepsubN  34518  pmapsub  34534  isline2  34540  linepmap  34541  isline3  34542  lncvrelatN  34547  2llnma1b  34552  cdlema1N  34557  cdlemblem  34559  cdlemb  34560  paddasslem5  34590  paddasslem12  34597  paddasslem13  34598  pmapjoin  34618  pmapjat1  34619  pmapjlln1  34621  hlmod1i  34622  llnmod1i2  34626  atmod2i1  34627  atmod2i2  34628  llnmod2i2  34629  atmod3i1  34630  atmod3i2  34631  dalawlem2  34638  dalawlem3  34639  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem11  34647  dalawlem12  34648  pmapocjN  34696  paddatclN  34715  linepsubclN  34717  pl42lem1N  34745  pl42lem2N  34746  pl42N  34749  lhp2lt  34767  lhpj1  34788  lhpmod2i2  34804  lhpmod6i1  34805  4atexlemc  34835  lautj  34859  trlval2  34930  trlcl  34931  trljat1  34933  trljat2  34934  trlle  34951  cdlemc1  34958  cdlemc2  34959  cdlemc5  34962  cdlemd2  34966  cdlemd3  34967  cdleme0aa  34977  cdleme0b  34979  cdleme0c  34980  cdleme0cp  34981  cdleme0cq  34982  cdleme0fN  34985  cdleme1b  34993  cdleme1  34994  cdleme2  34995  cdleme3b  34996  cdleme3c  34997  cdleme4a  35006  cdleme5  35007  cdleme7e  35014  cdleme8  35017  cdleme9  35020  cdleme10  35021  cdleme11fN  35031  cdleme11g  35032  cdleme11k  35035  cdleme11  35037  cdleme15b  35042  cdleme15  35045  cdleme22gb  35061  cdleme19b  35072  cdleme20d  35080  cdleme20j  35086  cdleme20l  35090  cdleme20m  35091  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f  35114  cdleme23b  35118  cdleme23c  35119  cdleme28a  35138  cdleme28b  35139  cdleme29ex  35142  cdleme30a  35146  cdlemefr29exN  35170  cdleme32e  35213  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme42e  35247  cdleme42i  35251  cdleme42mgN  35256  cdlemg2fv2  35368  cdlemg7fvbwN  35375  cdlemg4c  35380  cdlemg6c  35388  cdlemg10  35409  cdlemg11b  35410  cdlemg31a  35465  cdlemg31b  35466  cdlemg35  35481  trlcolem  35494  cdlemg44a  35499  trljco  35508  tendopltp  35548  cdlemh1  35583  cdlemh2  35584  cdlemi1  35586  cdlemi  35588  cdlemk4  35602  cdlemkvcl  35610  cdlemk10  35611  cdlemk11  35617  cdlemk11u  35639  cdlemk37  35682  cdlemkid1  35690  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  dialss  35815  dia2dimlem2  35834  dia2dimlem3  35835  cdlemm10N  35887  docaclN  35893  doca2N  35895  djajN  35906  diblss  35939  cdlemn2  35964  cdlemn10  35975  dihord1  35987  dihord2pre2  35995  dihord5apre  36031  dihjatc1  36080  dihmeetlem10N  36085  dihmeetlem11N  36086  djhljjN  36171  djhj  36173  dihprrnlem1N  36193  dihprrnlem2  36194  dihjat6  36203  dihjat5N  36206  dvh4dimat  36207
  Copyright terms: Public domain W3C validator