Theorem latjcl 17051

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

Syntax hints:   → wi 4   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  joincjn 16944  meetcmee 16945  Latclat 17045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-lub 16974  df-glb 16975  df-join 16976  df-meet 16977  df-lat 17046

This theorem is referenced by:  latleeqj1  17063  latjlej1  17065  latjlej12  17067  latnlej2  17071  latjidm  17074  latnle  17085  latabs2  17088  latledi  17089  latmlej11  17090  latjass  17095  latj13  17098  latj31  17099  latj4  17101  mod1ile  17105  mod2ile  17106  lubun  17123  latdisdlem  17189  oldmm1  34504  olj01  34512  latmassOLD  34516  omllaw5N  34534  cmtcomlemN  34535  cmtbr2N  34540  cmtbr3N  34541  cmtbr4N  34542  lecmtN  34543  omlfh1N  34545  omlfh3N  34546  omlmod1i2N  34547  cvlexchb1  34617  cvlcvr1  34626  hlatjcl  34653  exatleN  34690  cvrval3  34699  cvrexchlem  34705  cvrexch  34706  cvratlem  34707  cvrat  34708  lnnat  34713  cvrat2  34715  atcvrj2b  34718  atltcvr  34721  atlelt  34724  2atlt  34725  atexchcvrN  34726  cvrat3  34728  cvrat4  34729  2atjm  34731  4noncolr3  34739  athgt  34742  3dim0  34743  3dimlem4a  34749  1cvratex  34759  1cvrjat  34761  1cvrat  34762  ps-2  34764  3atlem1  34769  3atlem2  34770  3at  34776  2atm  34813  lplni2  34823  lplnle  34826  2llnmj  34846  2atmat  34847  lplnexllnN  34850  2llnjaN  34852  lvoli3  34863  islvol5  34865  lvoli2  34867  lvolnle3at  34868  3atnelvolN  34872  islvol2aN  34878  4atlem3  34882  4atlem4d  34888  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem11b  34894  4atlem11  34895  4atlem12a  34896  4atlem12b  34897  4atlem12  34898  4at  34899  lplncvrlvol2  34901  2lplnja  34905  2lplnmj  34908  dalem5  34953  dalem8  34956  dalem-cly  34957  dalem38  34996  dalem39  34997  dalem44  35002  dalem54  35012  linepsubN  35038  pmapsub  35054  isline2  35060  linepmap  35061  isline3  35062  lncvrelatN  35067  2llnma1b  35072  cdlema1N  35077  cdlemblem  35079  cdlemb  35080  paddasslem5  35110  paddasslem12  35117  paddasslem13  35118  pmapjoin  35138  pmapjat1  35139  pmapjlln1  35141  hlmod1i  35142  llnmod1i2  35146  atmod2i1  35147  atmod2i2  35148  llnmod2i2  35149  atmod3i1  35150  atmod3i2  35151  dalawlem2  35158  dalawlem3  35159  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem11  35167  dalawlem12  35168  pmapocjN  35216  paddatclN  35235  linepsubclN  35237  pl42lem1N  35265  pl42lem2N  35266  pl42N  35269  lhp2lt  35287  lhpj1  35308  lhpmod2i2  35324  lhpmod6i1  35325  4atexlemc  35355  lautj  35379  trlval2  35450  trlcl  35451  trljat1  35453  trljat2  35454  trlle  35471  cdlemc1  35478  cdlemc2  35479  cdlemc5  35482  cdlemd2  35486  cdlemd3  35487  cdleme0aa  35497  cdleme0b  35499  cdleme0c  35500  cdleme0cp  35501  cdleme0cq  35502  cdleme0fN  35505  cdleme1b  35513  cdleme1  35514  cdleme2  35515  cdleme3b  35516  cdleme3c  35517  cdleme4a  35526  cdleme5  35527  cdleme7e  35534  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme11fN  35551  cdleme11g  35552  cdleme11k  35555  cdleme11  35557  cdleme15b  35562  cdleme15  35565  cdleme22gb  35581  cdleme19b  35592  cdleme20d  35600  cdleme20j  35606  cdleme20l  35610  cdleme20m  35611  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme23b  35638  cdleme23c  35639  cdleme28a  35658  cdleme28b  35659  cdleme29ex  35662  cdleme30a  35666  cdlemefr29exN  35690  cdleme32e  35733  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme42e  35767  cdleme42i  35771  cdleme42mgN  35776  cdlemg2fv2  35888  cdlemg7fvbwN  35895  cdlemg4c  35900  cdlemg6c  35908  cdlemg10  35929  cdlemg11b  35930  cdlemg31a  35985  cdlemg31b  35986  cdlemg35  36001  trlcolem  36014  cdlemg44a  36019  trljco  36028  tendopltp  36068  cdlemh1  36103  cdlemh2  36104  cdlemi1  36106  cdlemi  36108  cdlemk4  36122  cdlemkvcl  36130  cdlemk10  36131  cdlemk11  36137  cdlemk11u  36159  cdlemk37  36202  cdlemkid1  36210  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  dialss  36335  dia2dimlem2  36354  dia2dimlem3  36355  cdlemm10N  36407  docaclN  36413  doca2N  36415  djajN  36426  diblss  36459  cdlemn2  36484  cdlemn10  36495  dihord1  36507  dihord2pre2  36515  dihord5apre  36551  dihjatc1  36600  dihmeetlem10N  36605  dihmeetlem11N  36606  djhljjN  36691  djhj  36693  dihprrnlem1N  36713  dihprrnlem2  36714  dihjat6  36723  dihjat5N  36726  dvh4dimat  36727