Theorem latjcl 18459

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ‘cfv 6553  (class class class)co 7423  Basecbs 17208  joincjn 18331  meetcmee 18332  Latclat 18451

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-lub 18366  df-glb 18367  df-join 18368  df-meet 18369  df-lat 18452

This theorem is referenced by:  latleeqj1  18471  latjlej1  18473  latjlej12  18475  latnlej2  18479  latjidm  18482  latnle  18493  latabs2  18496  latledi  18497  latmlej11  18498  latjass  18503  latj13  18506  latj31  18507  latj4  18509  mod1ile  18513  mod2ile  18514  latdisdlem  18516  lubun  18535  oldmm1  38863  olj01  38871  latmassOLD  38875  omllaw5N  38893  cmtcomlemN  38894  cmtbr2N  38899  cmtbr3N  38900  cmtbr4N  38901  lecmtN  38902  omlfh1N  38904  omlfh3N  38905  omlmod1i2N  38906  cvlexchb1  38976  cvlcvr1  38985  hlatjcl  39013  exatleN  39051  cvrval3  39060  cvrexchlem  39066  cvrexch  39067  cvratlem  39068  cvrat  39069  lnnat  39074  cvrat2  39076  atcvrj2b  39079  atltcvr  39082  atlelt  39085  2atlt  39086  atexchcvrN  39087  cvrat3  39089  cvrat4  39090  2atjm  39092  4noncolr3  39100  athgt  39103  3dim0  39104  3dimlem4a  39110  1cvratex  39120  1cvrjat  39122  1cvrat  39123  ps-2  39125  3atlem1  39130  3atlem2  39131  3at  39137  2atm  39174  lplni2  39184  lplnle  39187  2llnmj  39207  2atmat  39208  lplnexllnN  39211  2llnjaN  39213  lvoli3  39224  islvol5  39226  lvoli2  39228  lvolnle3at  39229  3atnelvolN  39233  islvol2aN  39239  4atlem3  39243  4atlem4d  39249  4atlem9  39250  4atlem10a  39251  4atlem10  39253  4atlem11a  39254  4atlem11b  39255  4atlem11  39256  4atlem12a  39257  4atlem12b  39258  4atlem12  39259  4at  39260  lplncvrlvol2  39262  2lplnja  39266  2lplnmj  39269  dalem5  39314  dalem8  39317  dalem-cly  39318  dalem38  39357  dalem39  39358  dalem44  39363  dalem54  39373  linepsubN  39399  pmapsub  39415  isline2  39421  linepmap  39422  isline3  39423  lncvrelatN  39428  2llnma1b  39433  cdlema1N  39438  cdlemblem  39440  cdlemb  39441  paddasslem5  39471  paddasslem12  39478  paddasslem13  39479  pmapjoin  39499  pmapjat1  39500  pmapjlln1  39502  hlmod1i  39503  llnmod1i2  39507  atmod2i1  39508  atmod2i2  39509  llnmod2i2  39510  atmod3i1  39511  atmod3i2  39512  dalawlem2  39519  dalawlem3  39520  dalawlem5  39522  dalawlem6  39523  dalawlem7  39524  dalawlem8  39525  dalawlem11  39528  dalawlem12  39529  pmapocjN  39577  paddatclN  39596  linepsubclN  39598  pl42lem1N  39626  pl42lem2N  39627  pl42N  39630  lhp2lt  39648  lhpj1  39669  lhpmod2i2  39685  lhpmod6i1  39686  4atexlemc  39716  lautj  39740  trlval2  39810  trlcl  39811  trljat1  39813  trljat2  39814  trlle  39831  cdlemc1  39838  cdlemc2  39839  cdlemc5  39842  cdlemd2  39846  cdlemd3  39847  cdleme0aa  39857  cdleme0b  39859  cdleme0c  39860  cdleme0cp  39861  cdleme0cq  39862  cdleme0fN  39865  cdleme1b  39873  cdleme1  39874  cdleme2  39875  cdleme3b  39876  cdleme3c  39877  cdleme4a  39886  cdleme5  39887  cdleme7e  39894  cdleme8  39897  cdleme9  39900  cdleme10  39901  cdleme11fN  39911  cdleme11g  39912  cdleme11k  39915  cdleme11  39917  cdleme15b  39922  cdleme15  39925  cdleme22gb  39941  cdleme19b  39951  cdleme20d  39959  cdleme20j  39965  cdleme20l  39969  cdleme20m  39970  cdleme22e  39991  cdleme22eALTN  39992  cdleme22f  39993  cdleme23b  39997  cdleme23c  39998  cdleme28a  40017  cdleme28b  40018  cdleme29ex  40021  cdleme30a  40025  cdlemefr29exN  40049  cdleme32e  40092  cdleme35fnpq  40096  cdleme35b  40097  cdleme35c  40098  cdleme42e  40126  cdleme42i  40130  cdleme42mgN  40135  cdlemg2fv2  40247  cdlemg7fvbwN  40254  cdlemg4c  40259  cdlemg6c  40267  cdlemg10  40288  cdlemg11b  40289  cdlemg31a  40344  cdlemg31b  40345  cdlemg35  40360  trlcolem  40373  cdlemg44a  40378  trljco  40387  tendopltp  40427  cdlemh1  40462  cdlemh2  40463  cdlemi1  40465  cdlemi  40467  cdlemk4  40481  cdlemkvcl  40489  cdlemk10  40490  cdlemk11  40496  cdlemk11u  40518  cdlemk37  40561  cdlemkid1  40569  cdlemk50  40599  cdlemk51  40600  cdlemk52  40601  dialss  40693  dia2dimlem2  40712  dia2dimlem3  40713  cdlemm10N  40765  docaclN  40771  doca2N  40773  djajN  40784  diblss  40817  cdlemn2  40842  cdlemn10  40853  dihord1  40865  dihord2pre2  40873  dihord5apre  40909  dihjatc1  40958  dihmeetlem10N  40963  dihmeetlem11N  40964  djhljjN  41049  djhj  41051  dihprrnlem1N  41071  dihprrnlem2  41072  dihjat6  41081  dihjat5N  41084  dvh4dimat  41085