Theorem latjcl 17663

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  joincjn 17556  meetcmee 17557  Latclat 17657

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-lub 17586  df-glb 17587  df-join 17588  df-meet 17589  df-lat 17658

This theorem is referenced by:  latleeqj1  17675  latjlej1  17677  latjlej12  17679  latnlej2  17683  latjidm  17686  latnle  17697  latabs2  17700  latledi  17701  latmlej11  17702  latjass  17707  latj13  17710  latj31  17711  latj4  17713  mod1ile  17717  mod2ile  17718  lubun  17735  latdisdlem  17801  oldmm1  36355  olj01  36363  latmassOLD  36367  omllaw5N  36385  cmtcomlemN  36386  cmtbr2N  36391  cmtbr3N  36392  cmtbr4N  36393  lecmtN  36394  omlfh1N  36396  omlfh3N  36397  omlmod1i2N  36398  cvlexchb1  36468  cvlcvr1  36477  hlatjcl  36505  exatleN  36542  cvrval3  36551  cvrexchlem  36557  cvrexch  36558  cvratlem  36559  cvrat  36560  lnnat  36565  cvrat2  36567  atcvrj2b  36570  atltcvr  36573  atlelt  36576  2atlt  36577  atexchcvrN  36578  cvrat3  36580  cvrat4  36581  2atjm  36583  4noncolr3  36591  athgt  36594  3dim0  36595  3dimlem4a  36601  1cvratex  36611  1cvrjat  36613  1cvrat  36614  ps-2  36616  3atlem1  36621  3atlem2  36622  3at  36628  2atm  36665  lplni2  36675  lplnle  36678  2llnmj  36698  2atmat  36699  lplnexllnN  36702  2llnjaN  36704  lvoli3  36715  islvol5  36717  lvoli2  36719  lvolnle3at  36720  3atnelvolN  36724  islvol2aN  36730  4atlem3  36734  4atlem4d  36740  4atlem9  36741  4atlem10a  36742  4atlem10  36744  4atlem11a  36745  4atlem11b  36746  4atlem11  36747  4atlem12a  36748  4atlem12b  36749  4atlem12  36750  4at  36751  lplncvrlvol2  36753  2lplnja  36757  2lplnmj  36760  dalem5  36805  dalem8  36808  dalem-cly  36809  dalem38  36848  dalem39  36849  dalem44  36854  dalem54  36864  linepsubN  36890  pmapsub  36906  isline2  36912  linepmap  36913  isline3  36914  lncvrelatN  36919  2llnma1b  36924  cdlema1N  36929  cdlemblem  36931  cdlemb  36932  paddasslem5  36962  paddasslem12  36969  paddasslem13  36970  pmapjoin  36990  pmapjat1  36991  pmapjlln1  36993  hlmod1i  36994  llnmod1i2  36998  atmod2i1  36999  atmod2i2  37000  llnmod2i2  37001  atmod3i1  37002  atmod3i2  37003  dalawlem2  37010  dalawlem3  37011  dalawlem5  37013  dalawlem6  37014  dalawlem7  37015  dalawlem8  37016  dalawlem11  37019  dalawlem12  37020  pmapocjN  37068  paddatclN  37087  linepsubclN  37089  pl42lem1N  37117  pl42lem2N  37118  pl42N  37121  lhp2lt  37139  lhpj1  37160  lhpmod2i2  37176  lhpmod6i1  37177  4atexlemc  37207  lautj  37231  trlval2  37301  trlcl  37302  trljat1  37304  trljat2  37305  trlle  37322  cdlemc1  37329  cdlemc2  37330  cdlemc5  37333  cdlemd2  37337  cdlemd3  37338  cdleme0aa  37348  cdleme0b  37350  cdleme0c  37351  cdleme0cp  37352  cdleme0cq  37353  cdleme0fN  37356  cdleme1b  37364  cdleme1  37365  cdleme2  37366  cdleme3b  37367  cdleme3c  37368  cdleme4a  37377  cdleme5  37378  cdleme7e  37385  cdleme8  37388  cdleme9  37391  cdleme10  37392  cdleme11fN  37402  cdleme11g  37403  cdleme11k  37406  cdleme11  37408  cdleme15b  37413  cdleme15  37416  cdleme22gb  37432  cdleme19b  37442  cdleme20d  37450  cdleme20j  37456  cdleme20l  37460  cdleme20m  37461  cdleme22e  37482  cdleme22eALTN  37483  cdleme22f  37484  cdleme23b  37488  cdleme23c  37489  cdleme28a  37508  cdleme28b  37509  cdleme29ex  37512  cdleme30a  37516  cdlemefr29exN  37540  cdleme32e  37583  cdleme35fnpq  37587  cdleme35b  37588  cdleme35c  37589  cdleme42e  37617  cdleme42i  37621  cdleme42mgN  37626  cdlemg2fv2  37738  cdlemg7fvbwN  37745  cdlemg4c  37750  cdlemg6c  37758  cdlemg10  37779  cdlemg11b  37780  cdlemg31a  37835  cdlemg31b  37836  cdlemg35  37851  trlcolem  37864  cdlemg44a  37869  trljco  37878  tendopltp  37918  cdlemh1  37953  cdlemh2  37954  cdlemi1  37956  cdlemi  37958  cdlemk4  37972  cdlemkvcl  37980  cdlemk10  37981  cdlemk11  37987  cdlemk11u  38009  cdlemk37  38052  cdlemkid1  38060  cdlemk50  38090  cdlemk51  38091  cdlemk52  38092  dialss  38184  dia2dimlem2  38203  dia2dimlem3  38204  cdlemm10N  38256  docaclN  38262  doca2N  38264  djajN  38275  diblss  38308  cdlemn2  38333  cdlemn10  38344  dihord1  38356  dihord2pre2  38364  dihord5apre  38400  dihjatc1  38449  dihmeetlem10N  38454  dihmeetlem11N  38455  djhljjN  38540  djhj  38542  dihprrnlem1N  38562  dihprrnlem2  38563  dihjat6  38572  dihjat5N  38575  dvh4dimat  38576