Theorem latjcl 18549

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6534  (class class class)co 7415  Basecbs 17323  joincjn 18421  meetcmee 18422  Latclat 18541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7372  df-ov 7418  df-oprab 7419  df-lub 18454  df-glb 18455  df-join 18456  df-meet 18457  df-lat 18542

This theorem is used by:  latleeqj1  18561  latjlej1  18563  latjlej12  18565  latnlej2  18569  latjidm  18572  latnle  18583  latabs2  18586  latledi  18587  latmlej11  18588  latjass  18593  latj13  18596  latj31  18597  latj4  18599  mod1ile  18603  mod2ile  18604  latdisdlem  18606  lubun  18625  oldmm1  40104  olj01  40112  latmassOLD  40116  omllaw5N  40134  cmtcomlemN  40135  cmtbr2N  40140  cmtbr3N  40141  cmtbr4N  40142  lecmtN  40143  omlfh1N  40145  omlfh3N  40146  omlmod1i2N  40147  cvlexchb1  40217  cvlcvr1  40226  hlatjcl  40254  exatleN  40291  cvrval3  40300  cvrexchlem  40306  cvrexch  40307  cvratlem  40308  cvrat  40309  lnnat  40314  cvrat2  40316  atcvrj2b  40319  atltcvr  40322  atlelt  40325  2atlt  40326  atexchcvrN  40327  cvrat3  40329  cvrat4  40330  2atjm  40332  4noncolr3  40340  athgt  40343  3dim0  40344  3dimlem4a  40350  1cvratex  40360  1cvrjat  40362  1cvrat  40363  ps-2  40365  3atlem1  40370  3atlem2  40371  3at  40377  2atm  40414  lplni2  40424  lplnle  40427  2llnmj  40447  2atmat  40448  lplnexllnN  40451  2llnjaN  40453  lvoli3  40464  islvol5  40466  lvoli2  40468  lvolnle3at  40469  3atnelvolN  40473  islvol2aN  40479  4atlem3  40483  4atlem4d  40489  4atlem9  40490  4atlem10a  40491  4atlem10  40493  4atlem11a  40494  4atlem11b  40495  4atlem11  40496  4atlem12a  40497  4atlem12b  40498  4atlem12  40499  4at  40500  lplncvrlvol2  40502  2lplnja  40506  2lplnmj  40509  dalem5  40554  dalem8  40557  dalem-cly  40558  dalem38  40597  dalem39  40598  dalem44  40603  dalem54  40613  linepsubN  40639  pmapsub  40655  isline2  40661  linepmap  40662  isline3  40663  lncvrelatN  40668  2llnma1b  40673  cdlema1N  40678  cdlemblem  40680  cdlemb  40681  paddasslem5  40711  paddasslem12  40718  paddasslem13  40719  pmapjoin  40739  pmapjat1  40740  pmapjlln1  40742  hlmod1i  40743  llnmod1i2  40747  atmod2i1  40748  atmod2i2  40749  llnmod2i2  40750  atmod3i1  40751  atmod3i2  40752  dalawlem2  40759  dalawlem3  40760  dalawlem5  40762  dalawlem6  40763  dalawlem7  40764  dalawlem8  40765  dalawlem11  40768  dalawlem12  40769  pmapocjN  40817  paddatclN  40836  linepsubclN  40838  pl42lem1N  40866  pl42lem2N  40867  pl42N  40870  lhp2lt  40888  lhpj1  40909  lhpmod2i2  40925  lhpmod6i1  40926  4atexlemc  40956  lautj  40980  trlval2  41050  trlcl  41051  trljat1  41053  trljat2  41054  trlle  41071  cdlemc1  41078  cdlemc2  41079  cdlemc5  41082  cdlemd2  41086  cdlemd3  41087  cdleme0aa  41097  cdleme0b  41099  cdleme0c  41100  cdleme0cp  41101  cdleme0cq  41102  cdleme0fN  41105  cdleme1b  41113  cdleme1  41114  cdleme2  41115  cdleme3b  41116  cdleme3c  41117  cdleme4a  41126  cdleme5  41127  cdleme7e  41134  cdleme8  41137  cdleme9  41140  cdleme10  41141  cdleme11fN  41151  cdleme11g  41152  cdleme11k  41155  cdleme11  41157  cdleme15b  41162  cdleme15  41165  cdleme22gb  41181  cdleme19b  41191  cdleme20d  41199  cdleme20j  41205  cdleme20l  41209  cdleme20m  41210  cdleme22e  41231  cdleme22eALTN  41232  cdleme22f  41233  cdleme23b  41237  cdleme23c  41238  cdleme28a  41257  cdleme28b  41258  cdleme29ex  41261  cdleme30a  41265  cdlemefr29exN  41289  cdleme32e  41332  cdleme35fnpq  41336  cdleme35b  41337  cdleme35c  41338  cdleme42e  41366  cdleme42i  41370  cdleme42mgN  41375  cdlemg2fv2  41487  cdlemg7fvbwN  41494  cdlemg4c  41499  cdlemg6c  41507  cdlemg10  41528  cdlemg11b  41529  cdlemg31a  41584  cdlemg31b  41585  cdlemg35  41600  trlcolem  41613  cdlemg44a  41618  trljco  41627  tendopltp  41667  cdlemh1  41702  cdlemh2  41703  cdlemi1  41705  cdlemi  41707  cdlemk4  41721  cdlemkvcl  41729  cdlemk10  41730  cdlemk11  41736  cdlemk11u  41758  cdlemk37  41801  cdlemkid1  41809  cdlemk50  41839  cdlemk51  41840  cdlemk52  41841  dialss  41933  dia2dimlem2  41952  dia2dimlem3  41953  cdlemm10N  42005  docaclN  42011  doca2N  42013  djajN  42024  diblss  42057  cdlemn2  42082  cdlemn10  42093  dihord1  42105  dihord2pre2  42113  dihord5apre  42149  dihjatc1  42198  dihmeetlem10N  42203  dihmeetlem11N  42204  djhljjN  42289  djhj  42291  dihprrnlem1N  42311  dihprrnlem2  42312  dihjat6  42321  dihjat5N  42324  dvh4dimat  42325