Theorem latjcl 18484

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  joincjn 18357  meetcmee 18358  Latclat 18476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-lub 18391  df-glb 18392  df-join 18393  df-meet 18394  df-lat 18477

This theorem is referenced by:  latleeqj1  18496  latjlej1  18498  latjlej12  18500  latnlej2  18504  latjidm  18507  latnle  18518  latabs2  18521  latledi  18522  latmlej11  18523  latjass  18528  latj13  18531  latj31  18532  latj4  18534  mod1ile  18538  mod2ile  18539  latdisdlem  18541  lubun  18560  oldmm1  39218  olj01  39226  latmassOLD  39230  omllaw5N  39248  cmtcomlemN  39249  cmtbr2N  39254  cmtbr3N  39255  cmtbr4N  39256  lecmtN  39257  omlfh1N  39259  omlfh3N  39260  omlmod1i2N  39261  cvlexchb1  39331  cvlcvr1  39340  hlatjcl  39368  exatleN  39406  cvrval3  39415  cvrexchlem  39421  cvrexch  39422  cvratlem  39423  cvrat  39424  lnnat  39429  cvrat2  39431  atcvrj2b  39434  atltcvr  39437  atlelt  39440  2atlt  39441  atexchcvrN  39442  cvrat3  39444  cvrat4  39445  2atjm  39447  4noncolr3  39455  athgt  39458  3dim0  39459  3dimlem4a  39465  1cvratex  39475  1cvrjat  39477  1cvrat  39478  ps-2  39480  3atlem1  39485  3atlem2  39486  3at  39492  2atm  39529  lplni2  39539  lplnle  39542  2llnmj  39562  2atmat  39563  lplnexllnN  39566  2llnjaN  39568  lvoli3  39579  islvol5  39581  lvoli2  39583  lvolnle3at  39584  3atnelvolN  39588  islvol2aN  39594  4atlem3  39598  4atlem4d  39604  4atlem9  39605  4atlem10a  39606  4atlem10  39608  4atlem11a  39609  4atlem11b  39610  4atlem11  39611  4atlem12a  39612  4atlem12b  39613  4atlem12  39614  4at  39615  lplncvrlvol2  39617  2lplnja  39621  2lplnmj  39624  dalem5  39669  dalem8  39672  dalem-cly  39673  dalem38  39712  dalem39  39713  dalem44  39718  dalem54  39728  linepsubN  39754  pmapsub  39770  isline2  39776  linepmap  39777  isline3  39778  lncvrelatN  39783  2llnma1b  39788  cdlema1N  39793  cdlemblem  39795  cdlemb  39796  paddasslem5  39826  paddasslem12  39833  paddasslem13  39834  pmapjoin  39854  pmapjat1  39855  pmapjlln1  39857  hlmod1i  39858  llnmod1i2  39862  atmod2i1  39863  atmod2i2  39864  llnmod2i2  39865  atmod3i1  39866  atmod3i2  39867  dalawlem2  39874  dalawlem3  39875  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem11  39883  dalawlem12  39884  pmapocjN  39932  paddatclN  39951  linepsubclN  39953  pl42lem1N  39981  pl42lem2N  39982  pl42N  39985  lhp2lt  40003  lhpj1  40024  lhpmod2i2  40040  lhpmod6i1  40041  4atexlemc  40071  lautj  40095  trlval2  40165  trlcl  40166  trljat1  40168  trljat2  40169  trlle  40186  cdlemc1  40193  cdlemc2  40194  cdlemc5  40197  cdlemd2  40201  cdlemd3  40202  cdleme0aa  40212  cdleme0b  40214  cdleme0c  40215  cdleme0cp  40216  cdleme0cq  40217  cdleme0fN  40220  cdleme1b  40228  cdleme1  40229  cdleme2  40230  cdleme3b  40231  cdleme3c  40232  cdleme4a  40241  cdleme5  40242  cdleme7e  40249  cdleme8  40252  cdleme9  40255  cdleme10  40256  cdleme11fN  40266  cdleme11g  40267  cdleme11k  40270  cdleme11  40272  cdleme15b  40277  cdleme15  40280  cdleme22gb  40296  cdleme19b  40306  cdleme20d  40314  cdleme20j  40320  cdleme20l  40324  cdleme20m  40325  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme23b  40352  cdleme23c  40353  cdleme28a  40372  cdleme28b  40373  cdleme29ex  40376  cdleme30a  40380  cdlemefr29exN  40404  cdleme32e  40447  cdleme35fnpq  40451  cdleme35b  40452  cdleme35c  40453  cdleme42e  40481  cdleme42i  40485  cdleme42mgN  40490  cdlemg2fv2  40602  cdlemg7fvbwN  40609  cdlemg4c  40614  cdlemg6c  40622  cdlemg10  40643  cdlemg11b  40644  cdlemg31a  40699  cdlemg31b  40700  cdlemg35  40715  trlcolem  40728  cdlemg44a  40733  trljco  40742  tendopltp  40782  cdlemh1  40817  cdlemh2  40818  cdlemi1  40820  cdlemi  40822  cdlemk4  40836  cdlemkvcl  40844  cdlemk10  40845  cdlemk11  40851  cdlemk11u  40873  cdlemk37  40916  cdlemkid1  40924  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  dialss  41048  dia2dimlem2  41067  dia2dimlem3  41068  cdlemm10N  41120  docaclN  41126  doca2N  41128  djajN  41139  diblss  41172  cdlemn2  41197  cdlemn10  41208  dihord1  41220  dihord2pre2  41228  dihord5apre  41264  dihjatc1  41313  dihmeetlem10N  41318  dihmeetlem11N  41319  djhljjN  41404  djhj  41406  dihprrnlem1N  41426  dihprrnlem2  41427  dihjat6  41436  dihjat5N  41439  dvh4dimat  41440