Theorem latjcl 18345

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6482  (class class class)co 7349  Basecbs 17120  joincjn 18217  meetcmee 18218  Latclat 18337

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-lub 18250  df-glb 18251  df-join 18252  df-meet 18253  df-lat 18338

This theorem is referenced by:  latleeqj1  18357  latjlej1  18359  latjlej12  18361  latnlej2  18365  latjidm  18368  latnle  18379  latabs2  18382  latledi  18383  latmlej11  18384  latjass  18389  latj13  18392  latj31  18393  latj4  18395  mod1ile  18399  mod2ile  18400  latdisdlem  18402  lubun  18421  oldmm1  39206  olj01  39214  latmassOLD  39218  omllaw5N  39236  cmtcomlemN  39237  cmtbr2N  39242  cmtbr3N  39243  cmtbr4N  39244  lecmtN  39245  omlfh1N  39247  omlfh3N  39248  omlmod1i2N  39249  cvlexchb1  39319  cvlcvr1  39328  hlatjcl  39356  exatleN  39393  cvrval3  39402  cvrexchlem  39408  cvrexch  39409  cvratlem  39410  cvrat  39411  lnnat  39416  cvrat2  39418  atcvrj2b  39421  atltcvr  39424  atlelt  39427  2atlt  39428  atexchcvrN  39429  cvrat3  39431  cvrat4  39432  2atjm  39434  4noncolr3  39442  athgt  39445  3dim0  39446  3dimlem4a  39452  1cvratex  39462  1cvrjat  39464  1cvrat  39465  ps-2  39467  3atlem1  39472  3atlem2  39473  3at  39479  2atm  39516  lplni2  39526  lplnle  39529  2llnmj  39549  2atmat  39550  lplnexllnN  39553  2llnjaN  39555  lvoli3  39566  islvol5  39568  lvoli2  39570  lvolnle3at  39571  3atnelvolN  39575  islvol2aN  39581  4atlem3  39585  4atlem4d  39591  4atlem9  39592  4atlem10a  39593  4atlem10  39595  4atlem11a  39596  4atlem11b  39597  4atlem11  39598  4atlem12a  39599  4atlem12b  39600  4atlem12  39601  4at  39602  lplncvrlvol2  39604  2lplnja  39608  2lplnmj  39611  dalem5  39656  dalem8  39659  dalem-cly  39660  dalem38  39699  dalem39  39700  dalem44  39705  dalem54  39715  linepsubN  39741  pmapsub  39757  isline2  39763  linepmap  39764  isline3  39765  lncvrelatN  39770  2llnma1b  39775  cdlema1N  39780  cdlemblem  39782  cdlemb  39783  paddasslem5  39813  paddasslem12  39820  paddasslem13  39821  pmapjoin  39841  pmapjat1  39842  pmapjlln1  39844  hlmod1i  39845  llnmod1i2  39849  atmod2i1  39850  atmod2i2  39851  llnmod2i2  39852  atmod3i1  39853  atmod3i2  39854  dalawlem2  39861  dalawlem3  39862  dalawlem5  39864  dalawlem6  39865  dalawlem7  39866  dalawlem8  39867  dalawlem11  39870  dalawlem12  39871  pmapocjN  39919  paddatclN  39938  linepsubclN  39940  pl42lem1N  39968  pl42lem2N  39969  pl42N  39972  lhp2lt  39990  lhpj1  40011  lhpmod2i2  40027  lhpmod6i1  40028  4atexlemc  40058  lautj  40082  trlval2  40152  trlcl  40153  trljat1  40155  trljat2  40156  trlle  40173  cdlemc1  40180  cdlemc2  40181  cdlemc5  40184  cdlemd2  40188  cdlemd3  40189  cdleme0aa  40199  cdleme0b  40201  cdleme0c  40202  cdleme0cp  40203  cdleme0cq  40204  cdleme0fN  40207  cdleme1b  40215  cdleme1  40216  cdleme2  40217  cdleme3b  40218  cdleme3c  40219  cdleme4a  40228  cdleme5  40229  cdleme7e  40236  cdleme8  40239  cdleme9  40242  cdleme10  40243  cdleme11fN  40253  cdleme11g  40254  cdleme11k  40257  cdleme11  40259  cdleme15b  40264  cdleme15  40267  cdleme22gb  40283  cdleme19b  40293  cdleme20d  40301  cdleme20j  40307  cdleme20l  40311  cdleme20m  40312  cdleme22e  40333  cdleme22eALTN  40334  cdleme22f  40335  cdleme23b  40339  cdleme23c  40340  cdleme28a  40359  cdleme28b  40360  cdleme29ex  40363  cdleme30a  40367  cdlemefr29exN  40391  cdleme32e  40434  cdleme35fnpq  40438  cdleme35b  40439  cdleme35c  40440  cdleme42e  40468  cdleme42i  40472  cdleme42mgN  40477  cdlemg2fv2  40589  cdlemg7fvbwN  40596  cdlemg4c  40601  cdlemg6c  40609  cdlemg10  40630  cdlemg11b  40631  cdlemg31a  40686  cdlemg31b  40687  cdlemg35  40702  trlcolem  40715  cdlemg44a  40720  trljco  40729  tendopltp  40769  cdlemh1  40804  cdlemh2  40805  cdlemi1  40807  cdlemi  40809  cdlemk4  40823  cdlemkvcl  40831  cdlemk10  40832  cdlemk11  40838  cdlemk11u  40860  cdlemk37  40903  cdlemkid1  40911  cdlemk50  40941  cdlemk51  40942  cdlemk52  40943  dialss  41035  dia2dimlem2  41054  dia2dimlem3  41055  cdlemm10N  41107  docaclN  41113  doca2N  41115  djajN  41126  diblss  41159  cdlemn2  41184  cdlemn10  41195  dihord1  41207  dihord2pre2  41215  dihord5apre  41251  dihjatc1  41300  dihmeetlem10N  41305  dihmeetlem11N  41306  djhljjN  41391  djhj  41393  dihprrnlem1N  41413  dihprrnlem2  41414  dihjat6  41423  dihjat5N  41426  dvh4dimat  41427