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

Theorem latjcl 17653
Description: Closure of join operation in a lattice. (chjcom 29289 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 2798 . . 3 (meet‘𝐾) = (meet‘𝐾)
41, 2, 3latlem 17651 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵))
54simpld 498 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2111  cfv 6324  (class class class)co 7135  Basecbs 16475  joincjn 17546  meetcmee 17547  Latclat 17647
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-lub 17576  df-glb 17577  df-join 17578  df-meet 17579  df-lat 17648
This theorem is referenced by:  latleeqj1  17665  latjlej1  17667  latjlej12  17669  latnlej2  17673  latjidm  17676  latnle  17687  latabs2  17690  latledi  17691  latmlej11  17692  latjass  17697  latj13  17700  latj31  17701  latj4  17703  mod1ile  17707  mod2ile  17708  lubun  17725  latdisdlem  17791  oldmm1  36513  olj01  36521  latmassOLD  36525  omllaw5N  36543  cmtcomlemN  36544  cmtbr2N  36549  cmtbr3N  36550  cmtbr4N  36551  lecmtN  36552  omlfh1N  36554  omlfh3N  36555  omlmod1i2N  36556  cvlexchb1  36626  cvlcvr1  36635  hlatjcl  36663  exatleN  36700  cvrval3  36709  cvrexchlem  36715  cvrexch  36716  cvratlem  36717  cvrat  36718  lnnat  36723  cvrat2  36725  atcvrj2b  36728  atltcvr  36731  atlelt  36734  2atlt  36735  atexchcvrN  36736  cvrat3  36738  cvrat4  36739  2atjm  36741  4noncolr3  36749  athgt  36752  3dim0  36753  3dimlem4a  36759  1cvratex  36769  1cvrjat  36771  1cvrat  36772  ps-2  36774  3atlem1  36779  3atlem2  36780  3at  36786  2atm  36823  lplni2  36833  lplnle  36836  2llnmj  36856  2atmat  36857  lplnexllnN  36860  2llnjaN  36862  lvoli3  36873  islvol5  36875  lvoli2  36877  lvolnle3at  36878  3atnelvolN  36882  islvol2aN  36888  4atlem3  36892  4atlem4d  36898  4atlem9  36899  4atlem10a  36900  4atlem10  36902  4atlem11a  36903  4atlem11b  36904  4atlem11  36905  4atlem12a  36906  4atlem12b  36907  4atlem12  36908  4at  36909  lplncvrlvol2  36911  2lplnja  36915  2lplnmj  36918  dalem5  36963  dalem8  36966  dalem-cly  36967  dalem38  37006  dalem39  37007  dalem44  37012  dalem54  37022  linepsubN  37048  pmapsub  37064  isline2  37070  linepmap  37071  isline3  37072  lncvrelatN  37077  2llnma1b  37082  cdlema1N  37087  cdlemblem  37089  cdlemb  37090  paddasslem5  37120  paddasslem12  37127  paddasslem13  37128  pmapjoin  37148  pmapjat1  37149  pmapjlln1  37151  hlmod1i  37152  llnmod1i2  37156  atmod2i1  37157  atmod2i2  37158  llnmod2i2  37159  atmod3i1  37160  atmod3i2  37161  dalawlem2  37168  dalawlem3  37169  dalawlem5  37171  dalawlem6  37172  dalawlem7  37173  dalawlem8  37174  dalawlem11  37177  dalawlem12  37178  pmapocjN  37226  paddatclN  37245  linepsubclN  37247  pl42lem1N  37275  pl42lem2N  37276  pl42N  37279  lhp2lt  37297  lhpj1  37318  lhpmod2i2  37334  lhpmod6i1  37335  4atexlemc  37365  lautj  37389  trlval2  37459  trlcl  37460  trljat1  37462  trljat2  37463  trlle  37480  cdlemc1  37487  cdlemc2  37488  cdlemc5  37491  cdlemd2  37495  cdlemd3  37496  cdleme0aa  37506  cdleme0b  37508  cdleme0c  37509  cdleme0cp  37510  cdleme0cq  37511  cdleme0fN  37514  cdleme1b  37522  cdleme1  37523  cdleme2  37524  cdleme3b  37525  cdleme3c  37526  cdleme4a  37535  cdleme5  37536  cdleme7e  37543  cdleme8  37546  cdleme9  37549  cdleme10  37550  cdleme11fN  37560  cdleme11g  37561  cdleme11k  37564  cdleme11  37566  cdleme15b  37571  cdleme15  37574  cdleme22gb  37590  cdleme19b  37600  cdleme20d  37608  cdleme20j  37614  cdleme20l  37618  cdleme20m  37619  cdleme22e  37640  cdleme22eALTN  37641  cdleme22f  37642  cdleme23b  37646  cdleme23c  37647  cdleme28a  37666  cdleme28b  37667  cdleme29ex  37670  cdleme30a  37674  cdlemefr29exN  37698  cdleme32e  37741  cdleme35fnpq  37745  cdleme35b  37746  cdleme35c  37747  cdleme42e  37775  cdleme42i  37779  cdleme42mgN  37784  cdlemg2fv2  37896  cdlemg7fvbwN  37903  cdlemg4c  37908  cdlemg6c  37916  cdlemg10  37937  cdlemg11b  37938  cdlemg31a  37993  cdlemg31b  37994  cdlemg35  38009  trlcolem  38022  cdlemg44a  38027  trljco  38036  tendopltp  38076  cdlemh1  38111  cdlemh2  38112  cdlemi1  38114  cdlemi  38116  cdlemk4  38130  cdlemkvcl  38138  cdlemk10  38139  cdlemk11  38145  cdlemk11u  38167  cdlemk37  38210  cdlemkid1  38218  cdlemk50  38248  cdlemk51  38249  cdlemk52  38250  dialss  38342  dia2dimlem2  38361  dia2dimlem3  38362  cdlemm10N  38414  docaclN  38420  doca2N  38422  djajN  38433  diblss  38466  cdlemn2  38491  cdlemn10  38502  dihord1  38514  dihord2pre2  38522  dihord5apre  38558  dihjatc1  38607  dihmeetlem10N  38612  dihmeetlem11N  38613  djhljjN  38698  djhj  38700  dihprrnlem1N  38720  dihprrnlem2  38721  dihjat6  38730  dihjat5N  38733  dvh4dimat  38734
  Copyright terms: Public domain W3C validator