Theorem latjcl 18072

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  joincjn 17944  meetcmee 17945  Latclat 18064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-lub 17979  df-glb 17980  df-join 17981  df-meet 17982  df-lat 18065

This theorem is referenced by:  latleeqj1  18084  latjlej1  18086  latjlej12  18088  latnlej2  18092  latjidm  18095  latnle  18106  latabs2  18109  latledi  18110  latmlej11  18111  latjass  18116  latj13  18119  latj31  18120  latj4  18122  mod1ile  18126  mod2ile  18127  latdisdlem  18129  lubun  18148  oldmm1  37158  olj01  37166  latmassOLD  37170  omllaw5N  37188  cmtcomlemN  37189  cmtbr2N  37194  cmtbr3N  37195  cmtbr4N  37196  lecmtN  37197  omlfh1N  37199  omlfh3N  37200  omlmod1i2N  37201  cvlexchb1  37271  cvlcvr1  37280  hlatjcl  37308  exatleN  37345  cvrval3  37354  cvrexchlem  37360  cvrexch  37361  cvratlem  37362  cvrat  37363  lnnat  37368  cvrat2  37370  atcvrj2b  37373  atltcvr  37376  atlelt  37379  2atlt  37380  atexchcvrN  37381  cvrat3  37383  cvrat4  37384  2atjm  37386  4noncolr3  37394  athgt  37397  3dim0  37398  3dimlem4a  37404  1cvratex  37414  1cvrjat  37416  1cvrat  37417  ps-2  37419  3atlem1  37424  3atlem2  37425  3at  37431  2atm  37468  lplni2  37478  lplnle  37481  2llnmj  37501  2atmat  37502  lplnexllnN  37505  2llnjaN  37507  lvoli3  37518  islvol5  37520  lvoli2  37522  lvolnle3at  37523  3atnelvolN  37527  islvol2aN  37533  4atlem3  37537  4atlem4d  37543  4atlem9  37544  4atlem10a  37545  4atlem10  37547  4atlem11a  37548  4atlem11b  37549  4atlem11  37550  4atlem12a  37551  4atlem12b  37552  4atlem12  37553  4at  37554  lplncvrlvol2  37556  2lplnja  37560  2lplnmj  37563  dalem5  37608  dalem8  37611  dalem-cly  37612  dalem38  37651  dalem39  37652  dalem44  37657  dalem54  37667  linepsubN  37693  pmapsub  37709  isline2  37715  linepmap  37716  isline3  37717  lncvrelatN  37722  2llnma1b  37727  cdlema1N  37732  cdlemblem  37734  cdlemb  37735  paddasslem5  37765  paddasslem12  37772  paddasslem13  37773  pmapjoin  37793  pmapjat1  37794  pmapjlln1  37796  hlmod1i  37797  llnmod1i2  37801  atmod2i1  37802  atmod2i2  37803  llnmod2i2  37804  atmod3i1  37805  atmod3i2  37806  dalawlem2  37813  dalawlem3  37814  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem11  37822  dalawlem12  37823  pmapocjN  37871  paddatclN  37890  linepsubclN  37892  pl42lem1N  37920  pl42lem2N  37921  pl42N  37924  lhp2lt  37942  lhpj1  37963  lhpmod2i2  37979  lhpmod6i1  37980  4atexlemc  38010  lautj  38034  trlval2  38104  trlcl  38105  trljat1  38107  trljat2  38108  trlle  38125  cdlemc1  38132  cdlemc2  38133  cdlemc5  38136  cdlemd2  38140  cdlemd3  38141  cdleme0aa  38151  cdleme0b  38153  cdleme0c  38154  cdleme0cp  38155  cdleme0cq  38156  cdleme0fN  38159  cdleme1b  38167  cdleme1  38168  cdleme2  38169  cdleme3b  38170  cdleme3c  38171  cdleme4a  38180  cdleme5  38181  cdleme7e  38188  cdleme8  38191  cdleme9  38194  cdleme10  38195  cdleme11fN  38205  cdleme11g  38206  cdleme11k  38209  cdleme11  38211  cdleme15b  38216  cdleme15  38219  cdleme22gb  38235  cdleme19b  38245  cdleme20d  38253  cdleme20j  38259  cdleme20l  38263  cdleme20m  38264  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme23b  38291  cdleme23c  38292  cdleme28a  38311  cdleme28b  38312  cdleme29ex  38315  cdleme30a  38319  cdlemefr29exN  38343  cdleme32e  38386  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme42e  38420  cdleme42i  38424  cdleme42mgN  38429  cdlemg2fv2  38541  cdlemg7fvbwN  38548  cdlemg4c  38553  cdlemg6c  38561  cdlemg10  38582  cdlemg11b  38583  cdlemg31a  38638  cdlemg31b  38639  cdlemg35  38654  trlcolem  38667  cdlemg44a  38672  trljco  38681  tendopltp  38721  cdlemh1  38756  cdlemh2  38757  cdlemi1  38759  cdlemi  38761  cdlemk4  38775  cdlemkvcl  38783  cdlemk10  38784  cdlemk11  38790  cdlemk11u  38812  cdlemk37  38855  cdlemkid1  38863  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  dialss  38987  dia2dimlem2  39006  dia2dimlem3  39007  cdlemm10N  39059  docaclN  39065  doca2N  39067  djajN  39078  diblss  39111  cdlemn2  39136  cdlemn10  39147  dihord1  39159  dihord2pre2  39167  dihord5apre  39203  dihjatc1  39252  dihmeetlem10N  39257  dihmeetlem11N  39258  djhljjN  39343  djhj  39345  dihprrnlem1N  39365  dihprrnlem2  39366  dihjat6  39375  dihjat5N  39378  dvh4dimat  39379