Theorem latjcl 18231

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ‘cfv 6465  (class class class)co 7316  Basecbs 16986  joincjn 18103  meetcmee 18104  Latclat 18223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7273  df-ov 7319  df-oprab 7320  df-lub 18138  df-glb 18139  df-join 18140  df-meet 18141  df-lat 18224

This theorem is referenced by:  latleeqj1  18243  latjlej1  18245  latjlej12  18247  latnlej2  18251  latjidm  18254  latnle  18265  latabs2  18268  latledi  18269  latmlej11  18270  latjass  18275  latj13  18278  latj31  18279  latj4  18281  mod1ile  18285  mod2ile  18286  latdisdlem  18288  lubun  18307  oldmm1  37456  olj01  37464  latmassOLD  37468  omllaw5N  37486  cmtcomlemN  37487  cmtbr2N  37492  cmtbr3N  37493  cmtbr4N  37494  lecmtN  37495  omlfh1N  37497  omlfh3N  37498  omlmod1i2N  37499  cvlexchb1  37569  cvlcvr1  37578  hlatjcl  37606  exatleN  37644  cvrval3  37653  cvrexchlem  37659  cvrexch  37660  cvratlem  37661  cvrat  37662  lnnat  37667  cvrat2  37669  atcvrj2b  37672  atltcvr  37675  atlelt  37678  2atlt  37679  atexchcvrN  37680  cvrat3  37682  cvrat4  37683  2atjm  37685  4noncolr3  37693  athgt  37696  3dim0  37697  3dimlem4a  37703  1cvratex  37713  1cvrjat  37715  1cvrat  37716  ps-2  37718  3atlem1  37723  3atlem2  37724  3at  37730  2atm  37767  lplni2  37777  lplnle  37780  2llnmj  37800  2atmat  37801  lplnexllnN  37804  2llnjaN  37806  lvoli3  37817  islvol5  37819  lvoli2  37821  lvolnle3at  37822  3atnelvolN  37826  islvol2aN  37832  4atlem3  37836  4atlem4d  37842  4atlem9  37843  4atlem10a  37844  4atlem10  37846  4atlem11a  37847  4atlem11b  37848  4atlem11  37849  4atlem12a  37850  4atlem12b  37851  4atlem12  37852  4at  37853  lplncvrlvol2  37855  2lplnja  37859  2lplnmj  37862  dalem5  37907  dalem8  37910  dalem-cly  37911  dalem38  37950  dalem39  37951  dalem44  37956  dalem54  37966  linepsubN  37992  pmapsub  38008  isline2  38014  linepmap  38015  isline3  38016  lncvrelatN  38021  2llnma1b  38026  cdlema1N  38031  cdlemblem  38033  cdlemb  38034  paddasslem5  38064  paddasslem12  38071  paddasslem13  38072  pmapjoin  38092  pmapjat1  38093  pmapjlln1  38095  hlmod1i  38096  llnmod1i2  38100  atmod2i1  38101  atmod2i2  38102  llnmod2i2  38103  atmod3i1  38104  atmod3i2  38105  dalawlem2  38112  dalawlem3  38113  dalawlem5  38115  dalawlem6  38116  dalawlem7  38117  dalawlem8  38118  dalawlem11  38121  dalawlem12  38122  pmapocjN  38170  paddatclN  38189  linepsubclN  38191  pl42lem1N  38219  pl42lem2N  38220  pl42N  38223  lhp2lt  38241  lhpj1  38262  lhpmod2i2  38278  lhpmod6i1  38279  4atexlemc  38309  lautj  38333  trlval2  38403  trlcl  38404  trljat1  38406  trljat2  38407  trlle  38424  cdlemc1  38431  cdlemc2  38432  cdlemc5  38435  cdlemd2  38439  cdlemd3  38440  cdleme0aa  38450  cdleme0b  38452  cdleme0c  38453  cdleme0cp  38454  cdleme0cq  38455  cdleme0fN  38458  cdleme1b  38466  cdleme1  38467  cdleme2  38468  cdleme3b  38469  cdleme3c  38470  cdleme4a  38479  cdleme5  38480  cdleme7e  38487  cdleme8  38490  cdleme9  38493  cdleme10  38494  cdleme11fN  38504  cdleme11g  38505  cdleme11k  38508  cdleme11  38510  cdleme15b  38515  cdleme15  38518  cdleme22gb  38534  cdleme19b  38544  cdleme20d  38552  cdleme20j  38558  cdleme20l  38562  cdleme20m  38563  cdleme22e  38584  cdleme22eALTN  38585  cdleme22f  38586  cdleme23b  38590  cdleme23c  38591  cdleme28a  38610  cdleme28b  38611  cdleme29ex  38614  cdleme30a  38618  cdlemefr29exN  38642  cdleme32e  38685  cdleme35fnpq  38689  cdleme35b  38690  cdleme35c  38691  cdleme42e  38719  cdleme42i  38723  cdleme42mgN  38728  cdlemg2fv2  38840  cdlemg7fvbwN  38847  cdlemg4c  38852  cdlemg6c  38860  cdlemg10  38881  cdlemg11b  38882  cdlemg31a  38937  cdlemg31b  38938  cdlemg35  38953  trlcolem  38966  cdlemg44a  38971  trljco  38980  tendopltp  39020  cdlemh1  39055  cdlemh2  39056  cdlemi1  39058  cdlemi  39060  cdlemk4  39074  cdlemkvcl  39082  cdlemk10  39083  cdlemk11  39089  cdlemk11u  39111  cdlemk37  39154  cdlemkid1  39162  cdlemk50  39192  cdlemk51  39193  cdlemk52  39194  dialss  39286  dia2dimlem2  39305  dia2dimlem3  39306  cdlemm10N  39358  docaclN  39364  doca2N  39366  djajN  39377  diblss  39410  cdlemn2  39435  cdlemn10  39446  dihord1  39458  dihord2pre2  39466  dihord5apre  39502  dihjatc1  39551  dihmeetlem10N  39556  dihmeetlem11N  39557  djhljjN  39642  djhj  39644  dihprrnlem1N  39664  dihprrnlem2  39665  dihjat6  39674  dihjat5N  39677  dvh4dimat  39678