Theorem latjcl 18473

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

Syntax hints:   → wi 4   ∧ w3a 1099   = wceq 1562   ∈ wcel 2144  ‘cfv 6523  (class class class)co 7398  Basecbs 17247  joincjn 18345  meetcmee 18346  Latclat 18465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-lub 18378  df-glb 18379  df-join 18380  df-meet 18381  df-lat 18466

This theorem is referenced by:  latleeqj1  18485  latjlej1  18487  latjlej12  18489  latnlej2  18493  latjidm  18496  latnle  18507  latabs2  18510  latledi  18511  latmlej11  18512  latjass  18517  latj13  18520  latj31  18521  latj4  18523  mod1ile  18527  mod2ile  18528  latdisdlem  18530  lubun  18549  oldmm1  39846  olj01  39854  latmassOLD  39858  omllaw5N  39876  cmtcomlemN  39877  cmtbr2N  39882  cmtbr3N  39883  cmtbr4N  39884  lecmtN  39885  omlfh1N  39887  omlfh3N  39888  omlmod1i2N  39889  cvlexchb1  39959  cvlcvr1  39968  hlatjcl  39996  exatleN  40033  cvrval3  40042  cvrexchlem  40048  cvrexch  40049  cvratlem  40050  cvrat  40051  lnnat  40056  cvrat2  40058  atcvrj2b  40061  atltcvr  40064  atlelt  40067  2atlt  40068  atexchcvrN  40069  cvrat3  40071  cvrat4  40072  2atjm  40074  4noncolr3  40082  athgt  40085  3dim0  40086  3dimlem4a  40092  1cvratex  40102  1cvrjat  40104  1cvrat  40105  ps-2  40107  3atlem1  40112  3atlem2  40113  3at  40119  2atm  40156  lplni2  40166  lplnle  40169  2llnmj  40189  2atmat  40190  lplnexllnN  40193  2llnjaN  40195  lvoli3  40206  islvol5  40208  lvoli2  40210  lvolnle3at  40211  3atnelvolN  40215  islvol2aN  40221  4atlem3  40225  4atlem4d  40231  4atlem9  40232  4atlem10a  40233  4atlem10  40235  4atlem11a  40236  4atlem11b  40237  4atlem11  40238  4atlem12a  40239  4atlem12b  40240  4atlem12  40241  4at  40242  lplncvrlvol2  40244  2lplnja  40248  2lplnmj  40251  dalem5  40296  dalem8  40299  dalem-cly  40300  dalem38  40339  dalem39  40340  dalem44  40345  dalem54  40355  linepsubN  40381  pmapsub  40397  isline2  40403  linepmap  40404  isline3  40405  lncvrelatN  40410  2llnma1b  40415  cdlema1N  40420  cdlemblem  40422  cdlemb  40423  paddasslem5  40453  paddasslem12  40460  paddasslem13  40461  pmapjoin  40481  pmapjat1  40482  pmapjlln1  40484  hlmod1i  40485  llnmod1i2  40489  atmod2i1  40490  atmod2i2  40491  llnmod2i2  40492  atmod3i1  40493  atmod3i2  40494  dalawlem2  40501  dalawlem3  40502  dalawlem5  40504  dalawlem6  40505  dalawlem7  40506  dalawlem8  40507  dalawlem11  40510  dalawlem12  40511  pmapocjN  40559  paddatclN  40578  linepsubclN  40580  pl42lem1N  40608  pl42lem2N  40609  pl42N  40612  lhp2lt  40630  lhpj1  40651  lhpmod2i2  40667  lhpmod6i1  40668  4atexlemc  40698  lautj  40722  trlval2  40792  trlcl  40793  trljat1  40795  trljat2  40796  trlle  40813  cdlemc1  40820  cdlemc2  40821  cdlemc5  40824  cdlemd2  40828  cdlemd3  40829  cdleme0aa  40839  cdleme0b  40841  cdleme0c  40842  cdleme0cp  40843  cdleme0cq  40844  cdleme0fN  40847  cdleme1b  40855  cdleme1  40856  cdleme2  40857  cdleme3b  40858  cdleme3c  40859  cdleme4a  40868  cdleme5  40869  cdleme7e  40876  cdleme8  40879  cdleme9  40882  cdleme10  40883  cdleme11fN  40893  cdleme11g  40894  cdleme11k  40897  cdleme11  40899  cdleme15b  40904  cdleme15  40907  cdleme22gb  40923  cdleme19b  40933  cdleme20d  40941  cdleme20j  40947  cdleme20l  40951  cdleme20m  40952  cdleme22e  40973  cdleme22eALTN  40974  cdleme22f  40975  cdleme23b  40979  cdleme23c  40980  cdleme28a  40999  cdleme28b  41000  cdleme29ex  41003  cdleme30a  41007  cdlemefr29exN  41031  cdleme32e  41074  cdleme35fnpq  41078  cdleme35b  41079  cdleme35c  41080  cdleme42e  41108  cdleme42i  41112  cdleme42mgN  41117  cdlemg2fv2  41229  cdlemg7fvbwN  41236  cdlemg4c  41241  cdlemg6c  41249  cdlemg10  41270  cdlemg11b  41271  cdlemg31a  41326  cdlemg31b  41327  cdlemg35  41342  trlcolem  41355  cdlemg44a  41360  trljco  41369  tendopltp  41409  cdlemh1  41444  cdlemh2  41445  cdlemi1  41447  cdlemi  41449  cdlemk4  41463  cdlemkvcl  41471  cdlemk10  41472  cdlemk11  41478  cdlemk11u  41500  cdlemk37  41543  cdlemkid1  41551  cdlemk50  41581  cdlemk51  41582  cdlemk52  41583  dialss  41675  dia2dimlem2  41694  dia2dimlem3  41695  cdlemm10N  41747  docaclN  41753  doca2N  41755  djajN  41766  diblss  41799  cdlemn2  41824  cdlemn10  41835  dihord1  41847  dihord2pre2  41855  dihord5apre  41891  dihjatc1  41940  dihmeetlem10N  41945  dihmeetlem11N  41946  djhljjN  42031  djhj  42033  dihprrnlem1N  42053  dihprrnlem2  42054  dihjat6  42063  dihjat5N  42066  dvh4dimat  42067