Theorem latjcl 16874

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

Syntax hints:   → wi 4   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  joincjn 16767  meetcmee 16768  Latclat 16868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-lub 16797  df-glb 16798  df-join 16799  df-meet 16800  df-lat 16869

This theorem is referenced by:  latleeqj1  16886  latjlej1  16888  latjlej12  16890  latnlej2  16894  latjidm  16897  latnle  16908  latabs2  16911  latledi  16912  latmlej11  16913  latjass  16918  latj13  16921  latj31  16922  latj4  16924  mod1ile  16928  mod2ile  16929  lubun  16946  latdisdlem  17012  oldmm1  33522  olj01  33530  latmassOLD  33534  omllaw5N  33552  cmtcomlemN  33553  cmtbr2N  33558  cmtbr3N  33559  cmtbr4N  33560  lecmtN  33561  omlfh1N  33563  omlfh3N  33564  omlmod1i2N  33565  cvlexchb1  33635  cvlcvr1  33644  hlatjcl  33671  exatleN  33708  cvrval3  33717  cvrexchlem  33723  cvrexch  33724  cvratlem  33725  cvrat  33726  lnnat  33731  cvrat2  33733  atcvrj2b  33736  atltcvr  33739  atlelt  33742  2atlt  33743  atexchcvrN  33744  cvrat3  33746  cvrat4  33747  2atjm  33749  4noncolr3  33757  athgt  33760  3dim0  33761  3dimlem4a  33767  1cvratex  33777  1cvrjat  33779  1cvrat  33780  ps-2  33782  3atlem1  33787  3atlem2  33788  3at  33794  2atm  33831  lplni2  33841  lplnle  33844  2llnmj  33864  2atmat  33865  lplnexllnN  33868  2llnjaN  33870  lvoli3  33881  islvol5  33883  lvoli2  33885  lvolnle3at  33886  3atnelvolN  33890  islvol2aN  33896  4atlem3  33900  4atlem4d  33906  4atlem9  33907  4atlem10a  33908  4atlem10  33910  4atlem11a  33911  4atlem11b  33912  4atlem11  33913  4atlem12a  33914  4atlem12b  33915  4atlem12  33916  4at  33917  lplncvrlvol2  33919  2lplnja  33923  2lplnmj  33926  dalem5  33971  dalem8  33974  dalem-cly  33975  dalem38  34014  dalem39  34015  dalem44  34020  dalem54  34030  linepsubN  34056  pmapsub  34072  isline2  34078  linepmap  34079  isline3  34080  lncvrelatN  34085  2llnma1b  34090  cdlema1N  34095  cdlemblem  34097  cdlemb  34098  paddasslem5  34128  paddasslem12  34135  paddasslem13  34136  pmapjoin  34156  pmapjat1  34157  pmapjlln1  34159  hlmod1i  34160  llnmod1i2  34164  atmod2i1  34165  atmod2i2  34166  llnmod2i2  34167  atmod3i1  34168  atmod3i2  34169  dalawlem2  34176  dalawlem3  34177  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem11  34185  dalawlem12  34186  pmapocjN  34234  paddatclN  34253  linepsubclN  34255  pl42lem1N  34283  pl42lem2N  34284  pl42N  34287  lhp2lt  34305  lhpj1  34326  lhpmod2i2  34342  lhpmod6i1  34343  4atexlemc  34373  lautj  34397  trlval2  34468  trlcl  34469  trljat1  34471  trljat2  34472  trlle  34489  cdlemc1  34496  cdlemc2  34497  cdlemc5  34500  cdlemd2  34504  cdlemd3  34505  cdleme0aa  34515  cdleme0b  34517  cdleme0c  34518  cdleme0cp  34519  cdleme0cq  34520  cdleme0fN  34523  cdleme1b  34531  cdleme1  34532  cdleme2  34533  cdleme3b  34534  cdleme3c  34535  cdleme4a  34544  cdleme5  34545  cdleme7e  34552  cdleme8  34555  cdleme9  34558  cdleme10  34559  cdleme11fN  34569  cdleme11g  34570  cdleme11k  34573  cdleme11  34575  cdleme15b  34580  cdleme15  34583  cdleme22gb  34599  cdleme19b  34610  cdleme20d  34618  cdleme20j  34624  cdleme20l  34628  cdleme20m  34629  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme23b  34656  cdleme23c  34657  cdleme28a  34676  cdleme28b  34677  cdleme29ex  34680  cdleme30a  34684  cdlemefr29exN  34708  cdleme32e  34751  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme42e  34785  cdleme42i  34789  cdleme42mgN  34794  cdlemg2fv2  34906  cdlemg7fvbwN  34913  cdlemg4c  34918  cdlemg6c  34926  cdlemg10  34947  cdlemg11b  34948  cdlemg31a  35003  cdlemg31b  35004  cdlemg35  35019  trlcolem  35032  cdlemg44a  35037  trljco  35046  tendopltp  35086  cdlemh1  35121  cdlemh2  35122  cdlemi1  35124  cdlemi  35126  cdlemk4  35140  cdlemkvcl  35148  cdlemk10  35149  cdlemk11  35155  cdlemk11u  35177  cdlemk37  35220  cdlemkid1  35228  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  dialss  35353  dia2dimlem2  35372  dia2dimlem3  35373  cdlemm10N  35425  docaclN  35431  doca2N  35433  djajN  35444  diblss  35477  cdlemn2  35502  cdlemn10  35513  dihord1  35525  dihord2pre2  35533  dihord5apre  35569  dihjatc1  35618  dihmeetlem10N  35623  dihmeetlem11N  35624  djhljjN  35709  djhj  35711  dihprrnlem1N  35731  dihprrnlem2  35732  dihjat6  35741  dihjat5N  35744  dvh4dimat  35745