Theorem latjcl 17250

Description: Closure of join operation in a lattice. (chjcom 28687 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 2802	. . 3 ⊢ (meet‘𝐾) = (meet‘𝐾)
4	1, 2, 3	latlem 17248	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵))
5	4	simpld 484	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1100   = wceq 1637   ∈ wcel 2155  ‘cfv 6095  (class class class)co 6868  Basecbs 16062  joincjn 17143  meetcmee 17144  Latclat 17244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-lub 17173  df-glb 17174  df-join 17175  df-meet 17176  df-lat 17245

This theorem is referenced by:  latleeqj1  17262  latjlej1  17264  latjlej12  17266  latnlej2  17270  latjidm  17273  latnle  17284  latabs2  17287  latledi  17288  latmlej11  17289  latjass  17294  latj13  17297  latj31  17298  latj4  17300  mod1ile  17304  mod2ile  17305  lubun  17322  latdisdlem  17388  oldmm1  34991  olj01  34999  latmassOLD  35003  omllaw5N  35021  cmtcomlemN  35022  cmtbr2N  35027  cmtbr3N  35028  cmtbr4N  35029  lecmtN  35030  omlfh1N  35032  omlfh3N  35033  omlmod1i2N  35034  cvlexchb1  35104  cvlcvr1  35113  hlatjcl  35141  exatleN  35178  cvrval3  35187  cvrexchlem  35193  cvrexch  35194  cvratlem  35195  cvrat  35196  lnnat  35201  cvrat2  35203  atcvrj2b  35206  atltcvr  35209  atlelt  35212  2atlt  35213  atexchcvrN  35214  cvrat3  35216  cvrat4  35217  2atjm  35219  4noncolr3  35227  athgt  35230  3dim0  35231  3dimlem4a  35237  1cvratex  35247  1cvrjat  35249  1cvrat  35250  ps-2  35252  3atlem1  35257  3atlem2  35258  3at  35264  2atm  35301  lplni2  35311  lplnle  35314  2llnmj  35334  2atmat  35335  lplnexllnN  35338  2llnjaN  35340  lvoli3  35351  islvol5  35353  lvoli2  35355  lvolnle3at  35356  3atnelvolN  35360  islvol2aN  35366  4atlem3  35370  4atlem4d  35376  4atlem9  35377  4atlem10a  35378  4atlem10  35380  4atlem11a  35381  4atlem11b  35382  4atlem11  35383  4atlem12a  35384  4atlem12b  35385  4atlem12  35386  4at  35387  lplncvrlvol2  35389  2lplnja  35393  2lplnmj  35396  dalem5  35441  dalem8  35444  dalem-cly  35445  dalem38  35484  dalem39  35485  dalem44  35490  dalem54  35500  linepsubN  35526  pmapsub  35542  isline2  35548  linepmap  35549  isline3  35550  lncvrelatN  35555  2llnma1b  35560  cdlema1N  35565  cdlemblem  35567  cdlemb  35568  paddasslem5  35598  paddasslem12  35605  paddasslem13  35606  pmapjoin  35626  pmapjat1  35627  pmapjlln1  35629  hlmod1i  35630  llnmod1i2  35634  atmod2i1  35635  atmod2i2  35636  llnmod2i2  35637  atmod3i1  35638  atmod3i2  35639  dalawlem2  35646  dalawlem3  35647  dalawlem5  35649  dalawlem6  35650  dalawlem7  35651  dalawlem8  35652  dalawlem11  35655  dalawlem12  35656  pmapocjN  35704  paddatclN  35723  linepsubclN  35725  pl42lem1N  35753  pl42lem2N  35754  pl42N  35757  lhp2lt  35775  lhpj1  35796  lhpmod2i2  35812  lhpmod6i1  35813  4atexlemc  35843  lautj  35867  trlval2  35938  trlcl  35939  trljat1  35941  trljat2  35942  trlle  35959  cdlemc1  35966  cdlemc2  35967  cdlemc5  35970  cdlemd2  35974  cdlemd3  35975  cdleme0aa  35985  cdleme0b  35987  cdleme0c  35988  cdleme0cp  35989  cdleme0cq  35990  cdleme0fN  35993  cdleme1b  36001  cdleme1  36002  cdleme2  36003  cdleme3b  36004  cdleme3c  36005  cdleme4a  36014  cdleme5  36015  cdleme7e  36022  cdleme8  36025  cdleme9  36028  cdleme10  36029  cdleme11fN  36039  cdleme11g  36040  cdleme11k  36043  cdleme11  36045  cdleme15b  36050  cdleme15  36053  cdleme22gb  36069  cdleme19b  36079  cdleme20d  36087  cdleme20j  36093  cdleme20l  36097  cdleme20m  36098  cdleme22e  36119  cdleme22eALTN  36120  cdleme22f  36121  cdleme23b  36125  cdleme23c  36126  cdleme28a  36145  cdleme28b  36146  cdleme29ex  36149  cdleme30a  36153  cdlemefr29exN  36177  cdleme32e  36220  cdleme35fnpq  36224  cdleme35b  36225  cdleme35c  36226  cdleme42e  36254  cdleme42i  36258  cdleme42mgN  36263  cdlemg2fv2  36375  cdlemg7fvbwN  36382  cdlemg4c  36387  cdlemg6c  36395  cdlemg10  36416  cdlemg11b  36417  cdlemg31a  36472  cdlemg31b  36473  cdlemg35  36488  trlcolem  36501  cdlemg44a  36506  trljco  36515  tendopltp  36555  cdlemh1  36590  cdlemh2  36591  cdlemi1  36593  cdlemi  36595  cdlemk4  36609  cdlemkvcl  36617  cdlemk10  36618  cdlemk11  36624  cdlemk11u  36646  cdlemk37  36689  cdlemkid1  36697  cdlemk50  36727  cdlemk51  36728  cdlemk52  36729  dialss  36821  dia2dimlem2  36840  dia2dimlem3  36841  cdlemm10N  36893  docaclN  36899  doca2N  36901  djajN  36912  diblss  36945  cdlemn2  36970  cdlemn10  36981  dihord1  36993  dihord2pre2  37001  dihord5apre  37037  dihjatc1  37086  dihmeetlem10N  37091  dihmeetlem11N  37092  djhljjN  37177  djhj  37179  dihprrnlem1N  37199  dihprrnlem2  37200  dihjat6  37209  dihjat5N  37212  dvh4dimat  37213