Theorem latjcl 18366

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  (class class class)co 7360  Basecbs 17140  joincjn 18238  meetcmee 18239  Latclat 18358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-lub 18271  df-glb 18272  df-join 18273  df-meet 18274  df-lat 18359

This theorem is referenced by:  latleeqj1  18378  latjlej1  18380  latjlej12  18382  latnlej2  18386  latjidm  18389  latnle  18400  latabs2  18403  latledi  18404  latmlej11  18405  latjass  18410  latj13  18413  latj31  18414  latj4  18416  mod1ile  18420  mod2ile  18421  latdisdlem  18423  lubun  18442  oldmm1  39545  olj01  39553  latmassOLD  39557  omllaw5N  39575  cmtcomlemN  39576  cmtbr2N  39581  cmtbr3N  39582  cmtbr4N  39583  lecmtN  39584  omlfh1N  39586  omlfh3N  39587  omlmod1i2N  39588  cvlexchb1  39658  cvlcvr1  39667  hlatjcl  39695  exatleN  39732  cvrval3  39741  cvrexchlem  39747  cvrexch  39748  cvratlem  39749  cvrat  39750  lnnat  39755  cvrat2  39757  atcvrj2b  39760  atltcvr  39763  atlelt  39766  2atlt  39767  atexchcvrN  39768  cvrat3  39770  cvrat4  39771  2atjm  39773  4noncolr3  39781  athgt  39784  3dim0  39785  3dimlem4a  39791  1cvratex  39801  1cvrjat  39803  1cvrat  39804  ps-2  39806  3atlem1  39811  3atlem2  39812  3at  39818  2atm  39855  lplni2  39865  lplnle  39868  2llnmj  39888  2atmat  39889  lplnexllnN  39892  2llnjaN  39894  lvoli3  39905  islvol5  39907  lvoli2  39909  lvolnle3at  39910  3atnelvolN  39914  islvol2aN  39920  4atlem3  39924  4atlem4d  39930  4atlem9  39931  4atlem10a  39932  4atlem10  39934  4atlem11a  39935  4atlem11b  39936  4atlem11  39937  4atlem12a  39938  4atlem12b  39939  4atlem12  39940  4at  39941  lplncvrlvol2  39943  2lplnja  39947  2lplnmj  39950  dalem5  39995  dalem8  39998  dalem-cly  39999  dalem38  40038  dalem39  40039  dalem44  40044  dalem54  40054  linepsubN  40080  pmapsub  40096  isline2  40102  linepmap  40103  isline3  40104  lncvrelatN  40109  2llnma1b  40114  cdlema1N  40119  cdlemblem  40121  cdlemb  40122  paddasslem5  40152  paddasslem12  40159  paddasslem13  40160  pmapjoin  40180  pmapjat1  40181  pmapjlln1  40183  hlmod1i  40184  llnmod1i2  40188  atmod2i1  40189  atmod2i2  40190  llnmod2i2  40191  atmod3i1  40192  atmod3i2  40193  dalawlem2  40200  dalawlem3  40201  dalawlem5  40203  dalawlem6  40204  dalawlem7  40205  dalawlem8  40206  dalawlem11  40209  dalawlem12  40210  pmapocjN  40258  paddatclN  40277  linepsubclN  40279  pl42lem1N  40307  pl42lem2N  40308  pl42N  40311  lhp2lt  40329  lhpj1  40350  lhpmod2i2  40366  lhpmod6i1  40367  4atexlemc  40397  lautj  40421  trlval2  40491  trlcl  40492  trljat1  40494  trljat2  40495  trlle  40512  cdlemc1  40519  cdlemc2  40520  cdlemc5  40523  cdlemd2  40527  cdlemd3  40528  cdleme0aa  40538  cdleme0b  40540  cdleme0c  40541  cdleme0cp  40542  cdleme0cq  40543  cdleme0fN  40546  cdleme1b  40554  cdleme1  40555  cdleme2  40556  cdleme3b  40557  cdleme3c  40558  cdleme4a  40567  cdleme5  40568  cdleme7e  40575  cdleme8  40578  cdleme9  40581  cdleme10  40582  cdleme11fN  40592  cdleme11g  40593  cdleme11k  40596  cdleme11  40598  cdleme15b  40603  cdleme15  40606  cdleme22gb  40622  cdleme19b  40632  cdleme20d  40640  cdleme20j  40646  cdleme20l  40650  cdleme20m  40651  cdleme22e  40672  cdleme22eALTN  40673  cdleme22f  40674  cdleme23b  40678  cdleme23c  40679  cdleme28a  40698  cdleme28b  40699  cdleme29ex  40702  cdleme30a  40706  cdlemefr29exN  40730  cdleme32e  40773  cdleme35fnpq  40777  cdleme35b  40778  cdleme35c  40779  cdleme42e  40807  cdleme42i  40811  cdleme42mgN  40816  cdlemg2fv2  40928  cdlemg7fvbwN  40935  cdlemg4c  40940  cdlemg6c  40948  cdlemg10  40969  cdlemg11b  40970  cdlemg31a  41025  cdlemg31b  41026  cdlemg35  41041  trlcolem  41054  cdlemg44a  41059  trljco  41068  tendopltp  41108  cdlemh1  41143  cdlemh2  41144  cdlemi1  41146  cdlemi  41148  cdlemk4  41162  cdlemkvcl  41170  cdlemk10  41171  cdlemk11  41177  cdlemk11u  41199  cdlemk37  41242  cdlemkid1  41250  cdlemk50  41280  cdlemk51  41281  cdlemk52  41282  dialss  41374  dia2dimlem2  41393  dia2dimlem3  41394  cdlemm10N  41446  docaclN  41452  doca2N  41454  djajN  41465  diblss  41498  cdlemn2  41523  cdlemn10  41534  dihord1  41546  dihord2pre2  41554  dihord5apre  41590  dihjatc1  41639  dihmeetlem10N  41644  dihmeetlem11N  41645  djhljjN  41730  djhj  41732  dihprrnlem1N  41752  dihprrnlem2  41753  dihjat6  41762  dihjat5N  41765  dvh4dimat  41766