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

Theorem latjcl 18396
Description: Closure of join operation in a lattice. (chjcom 31014 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 2732 . . 3 (meetβ€˜πΎ) = (meetβ€˜πΎ)
41, 2, 3latlem 18394 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ ((𝑋 ∨ π‘Œ) ∈ 𝐡 ∧ (𝑋(meetβ€˜πΎ)π‘Œ) ∈ 𝐡))
54simpld 495 1 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (𝑋 ∨ π‘Œ) ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  β€˜cfv 6543  (class class class)co 7411  Basecbs 17148  joincjn 18268  meetcmee 18269  Latclat 18388
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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-lat 18389
This theorem is referenced by:  latleeqj1  18408  latjlej1  18410  latjlej12  18412  latnlej2  18416  latjidm  18419  latnle  18430  latabs2  18433  latledi  18434  latmlej11  18435  latjass  18440  latj13  18443  latj31  18444  latj4  18446  mod1ile  18450  mod2ile  18451  latdisdlem  18453  lubun  18472  oldmm1  38390  olj01  38398  latmassOLD  38402  omllaw5N  38420  cmtcomlemN  38421  cmtbr2N  38426  cmtbr3N  38427  cmtbr4N  38428  lecmtN  38429  omlfh1N  38431  omlfh3N  38432  omlmod1i2N  38433  cvlexchb1  38503  cvlcvr1  38512  hlatjcl  38540  exatleN  38578  cvrval3  38587  cvrexchlem  38593  cvrexch  38594  cvratlem  38595  cvrat  38596  lnnat  38601  cvrat2  38603  atcvrj2b  38606  atltcvr  38609  atlelt  38612  2atlt  38613  atexchcvrN  38614  cvrat3  38616  cvrat4  38617  2atjm  38619  4noncolr3  38627  athgt  38630  3dim0  38631  3dimlem4a  38637  1cvratex  38647  1cvrjat  38649  1cvrat  38650  ps-2  38652  3atlem1  38657  3atlem2  38658  3at  38664  2atm  38701  lplni2  38711  lplnle  38714  2llnmj  38734  2atmat  38735  lplnexllnN  38738  2llnjaN  38740  lvoli3  38751  islvol5  38753  lvoli2  38755  lvolnle3at  38756  3atnelvolN  38760  islvol2aN  38766  4atlem3  38770  4atlem4d  38776  4atlem9  38777  4atlem10a  38778  4atlem10  38780  4atlem11a  38781  4atlem11b  38782  4atlem11  38783  4atlem12a  38784  4atlem12b  38785  4atlem12  38786  4at  38787  lplncvrlvol2  38789  2lplnja  38793  2lplnmj  38796  dalem5  38841  dalem8  38844  dalem-cly  38845  dalem38  38884  dalem39  38885  dalem44  38890  dalem54  38900  linepsubN  38926  pmapsub  38942  isline2  38948  linepmap  38949  isline3  38950  lncvrelatN  38955  2llnma1b  38960  cdlema1N  38965  cdlemblem  38967  cdlemb  38968  paddasslem5  38998  paddasslem12  39005  paddasslem13  39006  pmapjoin  39026  pmapjat1  39027  pmapjlln1  39029  hlmod1i  39030  llnmod1i2  39034  atmod2i1  39035  atmod2i2  39036  llnmod2i2  39037  atmod3i1  39038  atmod3i2  39039  dalawlem2  39046  dalawlem3  39047  dalawlem5  39049  dalawlem6  39050  dalawlem7  39051  dalawlem8  39052  dalawlem11  39055  dalawlem12  39056  pmapocjN  39104  paddatclN  39123  linepsubclN  39125  pl42lem1N  39153  pl42lem2N  39154  pl42N  39157  lhp2lt  39175  lhpj1  39196  lhpmod2i2  39212  lhpmod6i1  39213  4atexlemc  39243  lautj  39267  trlval2  39337  trlcl  39338  trljat1  39340  trljat2  39341  trlle  39358  cdlemc1  39365  cdlemc2  39366  cdlemc5  39369  cdlemd2  39373  cdlemd3  39374  cdleme0aa  39384  cdleme0b  39386  cdleme0c  39387  cdleme0cp  39388  cdleme0cq  39389  cdleme0fN  39392  cdleme1b  39400  cdleme1  39401  cdleme2  39402  cdleme3b  39403  cdleme3c  39404  cdleme4a  39413  cdleme5  39414  cdleme7e  39421  cdleme8  39424  cdleme9  39427  cdleme10  39428  cdleme11fN  39438  cdleme11g  39439  cdleme11k  39442  cdleme11  39444  cdleme15b  39449  cdleme15  39452  cdleme22gb  39468  cdleme19b  39478  cdleme20d  39486  cdleme20j  39492  cdleme20l  39496  cdleme20m  39497  cdleme22e  39518  cdleme22eALTN  39519  cdleme22f  39520  cdleme23b  39524  cdleme23c  39525  cdleme28a  39544  cdleme28b  39545  cdleme29ex  39548  cdleme30a  39552  cdlemefr29exN  39576  cdleme32e  39619  cdleme35fnpq  39623  cdleme35b  39624  cdleme35c  39625  cdleme42e  39653  cdleme42i  39657  cdleme42mgN  39662  cdlemg2fv2  39774  cdlemg7fvbwN  39781  cdlemg4c  39786  cdlemg6c  39794  cdlemg10  39815  cdlemg11b  39816  cdlemg31a  39871  cdlemg31b  39872  cdlemg35  39887  trlcolem  39900  cdlemg44a  39905  trljco  39914  tendopltp  39954  cdlemh1  39989  cdlemh2  39990  cdlemi1  39992  cdlemi  39994  cdlemk4  40008  cdlemkvcl  40016  cdlemk10  40017  cdlemk11  40023  cdlemk11u  40045  cdlemk37  40088  cdlemkid1  40096  cdlemk50  40126  cdlemk51  40127  cdlemk52  40128  dialss  40220  dia2dimlem2  40239  dia2dimlem3  40240  cdlemm10N  40292  docaclN  40298  doca2N  40300  djajN  40311  diblss  40344  cdlemn2  40369  cdlemn10  40380  dihord1  40392  dihord2pre2  40400  dihord5apre  40436  dihjatc1  40485  dihmeetlem10N  40490  dihmeetlem11N  40491  djhljjN  40576  djhj  40578  dihprrnlem1N  40598  dihprrnlem2  40599  dihjat6  40608  dihjat5N  40611  dvh4dimat  40612
  Copyright terms: Public domain W3C validator