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

Theorem latjcl 17252
Description: Closure of join operation in a lattice. (chjcom 28674 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 2760 . . 3 (meet‘𝐾) = (meet‘𝐾)
41, 2, 3latlem 17250 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵))
54simpld 477 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1632  wcel 2139  cfv 6049  (class class class)co 6813  Basecbs 16059  joincjn 17145  meetcmee 17146  Latclat 17246
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-lub 17175  df-glb 17176  df-join 17177  df-meet 17178  df-lat 17247
This theorem is referenced by:  latleeqj1  17264  latjlej1  17266  latjlej12  17268  latnlej2  17272  latjidm  17275  latnle  17286  latabs2  17289  latledi  17290  latmlej11  17291  latjass  17296  latj13  17299  latj31  17300  latj4  17302  mod1ile  17306  mod2ile  17307  lubun  17324  latdisdlem  17390  oldmm1  35007  olj01  35015  latmassOLD  35019  omllaw5N  35037  cmtcomlemN  35038  cmtbr2N  35043  cmtbr3N  35044  cmtbr4N  35045  lecmtN  35046  omlfh1N  35048  omlfh3N  35049  omlmod1i2N  35050  cvlexchb1  35120  cvlcvr1  35129  hlatjcl  35156  exatleN  35193  cvrval3  35202  cvrexchlem  35208  cvrexch  35209  cvratlem  35210  cvrat  35211  lnnat  35216  cvrat2  35218  atcvrj2b  35221  atltcvr  35224  atlelt  35227  2atlt  35228  atexchcvrN  35229  cvrat3  35231  cvrat4  35232  2atjm  35234  4noncolr3  35242  athgt  35245  3dim0  35246  3dimlem4a  35252  1cvratex  35262  1cvrjat  35264  1cvrat  35265  ps-2  35267  3atlem1  35272  3atlem2  35273  3at  35279  2atm  35316  lplni2  35326  lplnle  35329  2llnmj  35349  2atmat  35350  lplnexllnN  35353  2llnjaN  35355  lvoli3  35366  islvol5  35368  lvoli2  35370  lvolnle3at  35371  3atnelvolN  35375  islvol2aN  35381  4atlem3  35385  4atlem4d  35391  4atlem9  35392  4atlem10a  35393  4atlem10  35395  4atlem11a  35396  4atlem11b  35397  4atlem11  35398  4atlem12a  35399  4atlem12b  35400  4atlem12  35401  4at  35402  lplncvrlvol2  35404  2lplnja  35408  2lplnmj  35411  dalem5  35456  dalem8  35459  dalem-cly  35460  dalem38  35499  dalem39  35500  dalem44  35505  dalem54  35515  linepsubN  35541  pmapsub  35557  isline2  35563  linepmap  35564  isline3  35565  lncvrelatN  35570  2llnma1b  35575  cdlema1N  35580  cdlemblem  35582  cdlemb  35583  paddasslem5  35613  paddasslem12  35620  paddasslem13  35621  pmapjoin  35641  pmapjat1  35642  pmapjlln1  35644  hlmod1i  35645  llnmod1i2  35649  atmod2i1  35650  atmod2i2  35651  llnmod2i2  35652  atmod3i1  35653  atmod3i2  35654  dalawlem2  35661  dalawlem3  35662  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem11  35670  dalawlem12  35671  pmapocjN  35719  paddatclN  35738  linepsubclN  35740  pl42lem1N  35768  pl42lem2N  35769  pl42N  35772  lhp2lt  35790  lhpj1  35811  lhpmod2i2  35827  lhpmod6i1  35828  4atexlemc  35858  lautj  35882  trlval2  35953  trlcl  35954  trljat1  35956  trljat2  35957  trlle  35974  cdlemc1  35981  cdlemc2  35982  cdlemc5  35985  cdlemd2  35989  cdlemd3  35990  cdleme0aa  36000  cdleme0b  36002  cdleme0c  36003  cdleme0cp  36004  cdleme0cq  36005  cdleme0fN  36008  cdleme1b  36016  cdleme1  36017  cdleme2  36018  cdleme3b  36019  cdleme3c  36020  cdleme4a  36029  cdleme5  36030  cdleme7e  36037  cdleme8  36040  cdleme9  36043  cdleme10  36044  cdleme11fN  36054  cdleme11g  36055  cdleme11k  36058  cdleme11  36060  cdleme15b  36065  cdleme15  36068  cdleme22gb  36084  cdleme19b  36094  cdleme20d  36102  cdleme20j  36108  cdleme20l  36112  cdleme20m  36113  cdleme22e  36134  cdleme22eALTN  36135  cdleme22f  36136  cdleme23b  36140  cdleme23c  36141  cdleme28a  36160  cdleme28b  36161  cdleme29ex  36164  cdleme30a  36168  cdlemefr29exN  36192  cdleme32e  36235  cdleme35fnpq  36239  cdleme35b  36240  cdleme35c  36241  cdleme42e  36269  cdleme42i  36273  cdleme42mgN  36278  cdlemg2fv2  36390  cdlemg7fvbwN  36397  cdlemg4c  36402  cdlemg6c  36410  cdlemg10  36431  cdlemg11b  36432  cdlemg31a  36487  cdlemg31b  36488  cdlemg35  36503  trlcolem  36516  cdlemg44a  36521  trljco  36530  tendopltp  36570  cdlemh1  36605  cdlemh2  36606  cdlemi1  36608  cdlemi  36610  cdlemk4  36624  cdlemkvcl  36632  cdlemk10  36633  cdlemk11  36639  cdlemk11u  36661  cdlemk37  36704  cdlemkid1  36712  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  dialss  36837  dia2dimlem2  36856  dia2dimlem3  36857  cdlemm10N  36909  docaclN  36915  doca2N  36917  djajN  36928  diblss  36961  cdlemn2  36986  cdlemn10  36997  dihord1  37009  dihord2pre2  37017  dihord5apre  37053  dihjatc1  37102  dihmeetlem10N  37107  dihmeetlem11N  37108  djhljjN  37193  djhj  37195  dihprrnlem1N  37215  dihprrnlem2  37216  dihjat6  37225  dihjat5N  37228  dvh4dimat  37229
  Copyright terms: Public domain W3C validator