Theorem latjcl 18509

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  joincjn 18381  meetcmee 18382  Latclat 18501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-lub 18416  df-glb 18417  df-join 18418  df-meet 18419  df-lat 18502

This theorem is referenced by:  latleeqj1  18521  latjlej1  18523  latjlej12  18525  latnlej2  18529  latjidm  18532  latnle  18543  latabs2  18546  latledi  18547  latmlej11  18548  latjass  18553  latj13  18556  latj31  18557  latj4  18559  mod1ile  18563  mod2ile  18564  latdisdlem  18566  lubun  18585  oldmm1  39173  olj01  39181  latmassOLD  39185  omllaw5N  39203  cmtcomlemN  39204  cmtbr2N  39209  cmtbr3N  39210  cmtbr4N  39211  lecmtN  39212  omlfh1N  39214  omlfh3N  39215  omlmod1i2N  39216  cvlexchb1  39286  cvlcvr1  39295  hlatjcl  39323  exatleN  39361  cvrval3  39370  cvrexchlem  39376  cvrexch  39377  cvratlem  39378  cvrat  39379  lnnat  39384  cvrat2  39386  atcvrj2b  39389  atltcvr  39392  atlelt  39395  2atlt  39396  atexchcvrN  39397  cvrat3  39399  cvrat4  39400  2atjm  39402  4noncolr3  39410  athgt  39413  3dim0  39414  3dimlem4a  39420  1cvratex  39430  1cvrjat  39432  1cvrat  39433  ps-2  39435  3atlem1  39440  3atlem2  39441  3at  39447  2atm  39484  lplni2  39494  lplnle  39497  2llnmj  39517  2atmat  39518  lplnexllnN  39521  2llnjaN  39523  lvoli3  39534  islvol5  39536  lvoli2  39538  lvolnle3at  39539  3atnelvolN  39543  islvol2aN  39549  4atlem3  39553  4atlem4d  39559  4atlem9  39560  4atlem10a  39561  4atlem10  39563  4atlem11a  39564  4atlem11b  39565  4atlem11  39566  4atlem12a  39567  4atlem12b  39568  4atlem12  39569  4at  39570  lplncvrlvol2  39572  2lplnja  39576  2lplnmj  39579  dalem5  39624  dalem8  39627  dalem-cly  39628  dalem38  39667  dalem39  39668  dalem44  39673  dalem54  39683  linepsubN  39709  pmapsub  39725  isline2  39731  linepmap  39732  isline3  39733  lncvrelatN  39738  2llnma1b  39743  cdlema1N  39748  cdlemblem  39750  cdlemb  39751  paddasslem5  39781  paddasslem12  39788  paddasslem13  39789  pmapjoin  39809  pmapjat1  39810  pmapjlln1  39812  hlmod1i  39813  llnmod1i2  39817  atmod2i1  39818  atmod2i2  39819  llnmod2i2  39820  atmod3i1  39821  atmod3i2  39822  dalawlem2  39829  dalawlem3  39830  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem11  39838  dalawlem12  39839  pmapocjN  39887  paddatclN  39906  linepsubclN  39908  pl42lem1N  39936  pl42lem2N  39937  pl42N  39940  lhp2lt  39958  lhpj1  39979  lhpmod2i2  39995  lhpmod6i1  39996  4atexlemc  40026  lautj  40050  trlval2  40120  trlcl  40121  trljat1  40123  trljat2  40124  trlle  40141  cdlemc1  40148  cdlemc2  40149  cdlemc5  40152  cdlemd2  40156  cdlemd3  40157  cdleme0aa  40167  cdleme0b  40169  cdleme0c  40170  cdleme0cp  40171  cdleme0cq  40172  cdleme0fN  40175  cdleme1b  40183  cdleme1  40184  cdleme2  40185  cdleme3b  40186  cdleme3c  40187  cdleme4a  40196  cdleme5  40197  cdleme7e  40204  cdleme8  40207  cdleme9  40210  cdleme10  40211  cdleme11fN  40221  cdleme11g  40222  cdleme11k  40225  cdleme11  40227  cdleme15b  40232  cdleme15  40235  cdleme22gb  40251  cdleme19b  40261  cdleme20d  40269  cdleme20j  40275  cdleme20l  40279  cdleme20m  40280  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme23b  40307  cdleme23c  40308  cdleme28a  40327  cdleme28b  40328  cdleme29ex  40331  cdleme30a  40335  cdlemefr29exN  40359  cdleme32e  40402  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme42e  40436  cdleme42i  40440  cdleme42mgN  40445  cdlemg2fv2  40557  cdlemg7fvbwN  40564  cdlemg4c  40569  cdlemg6c  40577  cdlemg10  40598  cdlemg11b  40599  cdlemg31a  40654  cdlemg31b  40655  cdlemg35  40670  trlcolem  40683  cdlemg44a  40688  trljco  40697  tendopltp  40737  cdlemh1  40772  cdlemh2  40773  cdlemi1  40775  cdlemi  40777  cdlemk4  40791  cdlemkvcl  40799  cdlemk10  40800  cdlemk11  40806  cdlemk11u  40828  cdlemk37  40871  cdlemkid1  40879  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  dialss  41003  dia2dimlem2  41022  dia2dimlem3  41023  cdlemm10N  41075  docaclN  41081  doca2N  41083  djajN  41094  diblss  41127  cdlemn2  41152  cdlemn10  41163  dihord1  41175  dihord2pre2  41183  dihord5apre  41219  dihjatc1  41268  dihmeetlem10N  41273  dihmeetlem11N  41274  djhljjN  41359  djhj  41361  dihprrnlem1N  41381  dihprrnlem2  41382  dihjat6  41391  dihjat5N  41394  dvh4dimat  41395