Theorem latjcl 17661

Description: Closure of join operation in a lattice. (chjcom 29283 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

Step	Hyp	Ref	Expression
1		latjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		latjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
3		eqid 2821	. . 3 ⊢ (meet‘𝐾) = (meet‘𝐾)
4	1, 2, 3	latlem 17659	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵))
5	4	simpld 497	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  joincjn 17554  meetcmee 17555  Latclat 17655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-lub 17584  df-glb 17585  df-join 17586  df-meet 17587  df-lat 17656

This theorem is referenced by:  latleeqj1  17673  latjlej1  17675  latjlej12  17677  latnlej2  17681  latjidm  17684  latnle  17695  latabs2  17698  latledi  17699  latmlej11  17700  latjass  17705  latj13  17708  latj31  17709  latj4  17711  mod1ile  17715  mod2ile  17716  lubun  17733  latdisdlem  17799  oldmm1  36368  olj01  36376  latmassOLD  36380  omllaw5N  36398  cmtcomlemN  36399  cmtbr2N  36404  cmtbr3N  36405  cmtbr4N  36406  lecmtN  36407  omlfh1N  36409  omlfh3N  36410  omlmod1i2N  36411  cvlexchb1  36481  cvlcvr1  36490  hlatjcl  36518  exatleN  36555  cvrval3  36564  cvrexchlem  36570  cvrexch  36571  cvratlem  36572  cvrat  36573  lnnat  36578  cvrat2  36580  atcvrj2b  36583  atltcvr  36586  atlelt  36589  2atlt  36590  atexchcvrN  36591  cvrat3  36593  cvrat4  36594  2atjm  36596  4noncolr3  36604  athgt  36607  3dim0  36608  3dimlem4a  36614  1cvratex  36624  1cvrjat  36626  1cvrat  36627  ps-2  36629  3atlem1  36634  3atlem2  36635  3at  36641  2atm  36678  lplni2  36688  lplnle  36691  2llnmj  36711  2atmat  36712  lplnexllnN  36715  2llnjaN  36717  lvoli3  36728  islvol5  36730  lvoli2  36732  lvolnle3at  36733  3atnelvolN  36737  islvol2aN  36743  4atlem3  36747  4atlem4d  36753  4atlem9  36754  4atlem10a  36755  4atlem10  36757  4atlem11a  36758  4atlem11b  36759  4atlem11  36760  4atlem12a  36761  4atlem12b  36762  4atlem12  36763  4at  36764  lplncvrlvol2  36766  2lplnja  36770  2lplnmj  36773  dalem5  36818  dalem8  36821  dalem-cly  36822  dalem38  36861  dalem39  36862  dalem44  36867  dalem54  36877  linepsubN  36903  pmapsub  36919  isline2  36925  linepmap  36926  isline3  36927  lncvrelatN  36932  2llnma1b  36937  cdlema1N  36942  cdlemblem  36944  cdlemb  36945  paddasslem5  36975  paddasslem12  36982  paddasslem13  36983  pmapjoin  37003  pmapjat1  37004  pmapjlln1  37006  hlmod1i  37007  llnmod1i2  37011  atmod2i1  37012  atmod2i2  37013  llnmod2i2  37014  atmod3i1  37015  atmod3i2  37016  dalawlem2  37023  dalawlem3  37024  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem11  37032  dalawlem12  37033  pmapocjN  37081  paddatclN  37100  linepsubclN  37102  pl42lem1N  37130  pl42lem2N  37131  pl42N  37134  lhp2lt  37152  lhpj1  37173  lhpmod2i2  37189  lhpmod6i1  37190  4atexlemc  37220  lautj  37244  trlval2  37314  trlcl  37315  trljat1  37317  trljat2  37318  trlle  37335  cdlemc1  37342  cdlemc2  37343  cdlemc5  37346  cdlemd2  37350  cdlemd3  37351  cdleme0aa  37361  cdleme0b  37363  cdleme0c  37364  cdleme0cp  37365  cdleme0cq  37366  cdleme0fN  37369  cdleme1b  37377  cdleme1  37378  cdleme2  37379  cdleme3b  37380  cdleme3c  37381  cdleme4a  37390  cdleme5  37391  cdleme7e  37398  cdleme8  37401  cdleme9  37404  cdleme10  37405  cdleme11fN  37415  cdleme11g  37416  cdleme11k  37419  cdleme11  37421  cdleme15b  37426  cdleme15  37429  cdleme22gb  37445  cdleme19b  37455  cdleme20d  37463  cdleme20j  37469  cdleme20l  37473  cdleme20m  37474  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme23b  37501  cdleme23c  37502  cdleme28a  37521  cdleme28b  37522  cdleme29ex  37525  cdleme30a  37529  cdlemefr29exN  37553  cdleme32e  37596  cdleme35fnpq  37600  cdleme35b  37601  cdleme35c  37602  cdleme42e  37630  cdleme42i  37634  cdleme42mgN  37639  cdlemg2fv2  37751  cdlemg7fvbwN  37758  cdlemg4c  37763  cdlemg6c  37771  cdlemg10  37792  cdlemg11b  37793  cdlemg31a  37848  cdlemg31b  37849  cdlemg35  37864  trlcolem  37877  cdlemg44a  37882  trljco  37891  tendopltp  37931  cdlemh1  37966  cdlemh2  37967  cdlemi1  37969  cdlemi  37971  cdlemk4  37985  cdlemkvcl  37993  cdlemk10  37994  cdlemk11  38000  cdlemk11u  38022  cdlemk37  38065  cdlemkid1  38073  cdlemk50  38103  cdlemk51  38104  cdlemk52  38105  dialss  38197  dia2dimlem2  38216  dia2dimlem3  38217  cdlemm10N  38269  docaclN  38275  doca2N  38277  djajN  38288  diblss  38321  cdlemn2  38346  cdlemn10  38357  dihord1  38369  dihord2pre2  38377  dihord5apre  38413  dihjatc1  38462  dihmeetlem10N  38467  dihmeetlem11N  38468  djhljjN  38553  djhj  38555  dihprrnlem1N  38575  dihprrnlem2  38576  dihjat6  38585  dihjat5N  38588  dvh4dimat  38589