Theorem latjcl 18166

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  joincjn 18038  meetcmee 18039  Latclat 18158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-lub 18073  df-glb 18074  df-join 18075  df-meet 18076  df-lat 18159

This theorem is referenced by:  latleeqj1  18178  latjlej1  18180  latjlej12  18182  latnlej2  18186  latjidm  18189  latnle  18200  latabs2  18203  latledi  18204  latmlej11  18205  latjass  18210  latj13  18213  latj31  18214  latj4  18216  mod1ile  18220  mod2ile  18221  latdisdlem  18223  lubun  18242  oldmm1  37238  olj01  37246  latmassOLD  37250  omllaw5N  37268  cmtcomlemN  37269  cmtbr2N  37274  cmtbr3N  37275  cmtbr4N  37276  lecmtN  37277  omlfh1N  37279  omlfh3N  37280  omlmod1i2N  37281  cvlexchb1  37351  cvlcvr1  37360  hlatjcl  37388  exatleN  37425  cvrval3  37434  cvrexchlem  37440  cvrexch  37441  cvratlem  37442  cvrat  37443  lnnat  37448  cvrat2  37450  atcvrj2b  37453  atltcvr  37456  atlelt  37459  2atlt  37460  atexchcvrN  37461  cvrat3  37463  cvrat4  37464  2atjm  37466  4noncolr3  37474  athgt  37477  3dim0  37478  3dimlem4a  37484  1cvratex  37494  1cvrjat  37496  1cvrat  37497  ps-2  37499  3atlem1  37504  3atlem2  37505  3at  37511  2atm  37548  lplni2  37558  lplnle  37561  2llnmj  37581  2atmat  37582  lplnexllnN  37585  2llnjaN  37587  lvoli3  37598  islvol5  37600  lvoli2  37602  lvolnle3at  37603  3atnelvolN  37607  islvol2aN  37613  4atlem3  37617  4atlem4d  37623  4atlem9  37624  4atlem10a  37625  4atlem10  37627  4atlem11a  37628  4atlem11b  37629  4atlem11  37630  4atlem12a  37631  4atlem12b  37632  4atlem12  37633  4at  37634  lplncvrlvol2  37636  2lplnja  37640  2lplnmj  37643  dalem5  37688  dalem8  37691  dalem-cly  37692  dalem38  37731  dalem39  37732  dalem44  37737  dalem54  37747  linepsubN  37773  pmapsub  37789  isline2  37795  linepmap  37796  isline3  37797  lncvrelatN  37802  2llnma1b  37807  cdlema1N  37812  cdlemblem  37814  cdlemb  37815  paddasslem5  37845  paddasslem12  37852  paddasslem13  37853  pmapjoin  37873  pmapjat1  37874  pmapjlln1  37876  hlmod1i  37877  llnmod1i2  37881  atmod2i1  37882  atmod2i2  37883  llnmod2i2  37884  atmod3i1  37885  atmod3i2  37886  dalawlem2  37893  dalawlem3  37894  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem11  37902  dalawlem12  37903  pmapocjN  37951  paddatclN  37970  linepsubclN  37972  pl42lem1N  38000  pl42lem2N  38001  pl42N  38004  lhp2lt  38022  lhpj1  38043  lhpmod2i2  38059  lhpmod6i1  38060  4atexlemc  38090  lautj  38114  trlval2  38184  trlcl  38185  trljat1  38187  trljat2  38188  trlle  38205  cdlemc1  38212  cdlemc2  38213  cdlemc5  38216  cdlemd2  38220  cdlemd3  38221  cdleme0aa  38231  cdleme0b  38233  cdleme0c  38234  cdleme0cp  38235  cdleme0cq  38236  cdleme0fN  38239  cdleme1b  38247  cdleme1  38248  cdleme2  38249  cdleme3b  38250  cdleme3c  38251  cdleme4a  38260  cdleme5  38261  cdleme7e  38268  cdleme8  38271  cdleme9  38274  cdleme10  38275  cdleme11fN  38285  cdleme11g  38286  cdleme11k  38289  cdleme11  38291  cdleme15b  38296  cdleme15  38299  cdleme22gb  38315  cdleme19b  38325  cdleme20d  38333  cdleme20j  38339  cdleme20l  38343  cdleme20m  38344  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme23b  38371  cdleme23c  38372  cdleme28a  38391  cdleme28b  38392  cdleme29ex  38395  cdleme30a  38399  cdlemefr29exN  38423  cdleme32e  38466  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme42e  38500  cdleme42i  38504  cdleme42mgN  38509  cdlemg2fv2  38621  cdlemg7fvbwN  38628  cdlemg4c  38633  cdlemg6c  38641  cdlemg10  38662  cdlemg11b  38663  cdlemg31a  38718  cdlemg31b  38719  cdlemg35  38734  trlcolem  38747  cdlemg44a  38752  trljco  38761  tendopltp  38801  cdlemh1  38836  cdlemh2  38837  cdlemi1  38839  cdlemi  38841  cdlemk4  38855  cdlemkvcl  38863  cdlemk10  38864  cdlemk11  38870  cdlemk11u  38892  cdlemk37  38935  cdlemkid1  38943  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  dialss  39067  dia2dimlem2  39086  dia2dimlem3  39087  cdlemm10N  39139  docaclN  39145  doca2N  39147  djajN  39158  diblss  39191  cdlemn2  39216  cdlemn10  39227  dihord1  39239  dihord2pre2  39247  dihord5apre  39283  dihjatc1  39332  dihmeetlem10N  39337  dihmeetlem11N  39338  djhljjN  39423  djhj  39425  dihprrnlem1N  39445  dihprrnlem2  39446  dihjat6  39455  dihjat5N  39458  dvh4dimat  39459