Theorem hlatjcl 39813

Description: Closure of join operation. Frequently-used special case of latjcl 18405 for atoms. (Contributed by NM, 15-Jun-2012.)

Hypotheses

Ref	Expression
hlatjcl.b	⊢ 𝐵 = (Base‘𝐾)
hlatjcl.j	⊢ ∨ = (join‘𝐾)
hlatjcl.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
hlatjcl	⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Proof of Theorem hlatjcl

Step	Hyp	Ref	Expression
1		hllat 39809	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39735	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 39735	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18405	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	1, 4, 5, 7	syl3an 1161	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  joincjn 18277  Latclat 18397  Atomscatm 39709  HLchlt 39796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-lub 18310  df-glb 18311  df-join 18312  df-meet 18313  df-lat 18398  df-ats 39713  df-atl 39744  df-cvlat 39768  df-hlat 39797

This theorem is referenced by:  atcvr0eq  39872  2atjm  39891  atbtwn  39892  3dim0  39903  3dimlem3a  39906  3dimlem3OLDN  39908  3dimlem4OLDN  39911  3dim3  39915  2dim  39916  ps-1  39923  hlatexch3N  39926  hlatexch4  39927  ps-2b  39928  3atlem1  39929  3atlem2  39930  llni2  39958  llnle  39964  2at0mat0  39971  2atm  39973  islpln5  39981  lplni2  39983  lplnnle2at  39987  2atnelpln  39990  islpln2a  39994  llncvrlpln2  40003  2atmat  40007  2llnjaN  40012  islvol5  40025  lvoli2  40027  lvolnle3at  40028  3atnelvolN  40032  islvol2aN  40038  4atlem0a  40039  4atlem3  40042  4atlem3a  40043  4atlem3b  40044  4atlem4a  40045  4atlem4b  40046  4atlem4c  40047  4atlem4d  40048  4atlem9  40049  4atlem10a  40050  4atlem10  40052  4atlem11a  40053  4atlem11b  40054  4atlem11  40055  4atlem12a  40056  4atlem12b  40057  4atlem12  40058  4at  40059  4at2  40060  lplncvrlvol2  40061  2lplnja  40065  dalempjqeb  40091  dalemsjteb  40092  dalemtjueb  40093  dalemply  40100  dalem1  40105  dalemcea  40106  dalem3  40110  dalem4  40111  dalem5  40113  dalem-cly  40117  dalem17  40126  dalem21  40140  dalem24  40143  dalem25  40144  dalem27  40145  dalem38  40156  dalem39  40157  dalem43  40161  dalem44  40162  dalem45  40163  dalem55  40173  dalem56  40174  dalem57  40175  2atm2atN  40231  2llnma1b  40232  2llnma3r  40234  llnmod2i2  40309  llnexchb2lem  40314  dalawlem1  40317  dalawlem2  40318  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  dalawlem15  40331  lhp2lt  40447  lhpexle2lem  40455  lhpexle3lem  40457  lhp2at0  40478  lhp2atnle  40479  lhpat3  40492  4atexlempsb  40506  4atexlemqtb  40507  4atexlemunv  40512  4atexlemtlw  40513  4atexlemc  40515  4atexlemnclw  40516  4atexlemcnd  40518  trlval3  40633  trlval4  40634  cdlemc4  40640  cdlemc5  40641  cdlemc6  40642  cdlemd2  40645  cdleme0e  40663  cdlemeulpq  40666  cdleme01N  40667  cdleme0ex1N  40669  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme4  40684  cdleme4a  40685  cdleme5  40686  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme9b  40698  cdleme9  40699  cdleme10  40700  cdleme11c  40707  cdleme13  40718  cdleme15b  40721  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16e  40728  cdleme16f  40729  cdleme17b  40733  cdleme22gb  40740  cdlemedb  40743  cdlemednpq  40745  cdleme20zN  40747  cdleme19a  40749  cdleme19c  40751  cdleme20aN  40755  cdleme20c  40757  cdleme20d  40758  cdleme20e  40759  cdleme20j  40764  cdleme20l  40768  cdleme21c  40773  cdleme21ct  40775  cdleme22aa  40785  cdleme22b  40787  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme22g  40794  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme28a  40816  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme35f  40900  cdleme42a  40917  cdleme42c  40918  cdleme42h  40928  cdleme42i  40929  cdlemeg46frv  40971  cdlemeg46vrg  40973  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemf1  41007  cdlemf2  41008  cdlemg2fv2  41046  cdlemg2m  41050  cdlemg4  41063  cdlemg8b  41074  cdlemg10bALTN  41082  cdlemg10c  41085  cdlemg10  41087  cdlemg12e  41093  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg17a  41107  cdlemg17dALTN  41110  cdlemg17h  41114  cdlemg17  41123  cdlemg18b  41125  cdlemg19a  41129  cdlemg19  41130  cdlemg27a  41138  cdlemg27b  41142  cdlemg31a  41143  cdlemg31b  41144  cdlemg33b0  41147  cdlemg33a  41152  trlcoabs2N  41168  trlcolem  41172  cdlemg42  41175  cdlemg46  41181  cdlemh1  41261  cdlemk3  41279  cdlemk10  41289  cdlemk12  41296  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk1u  41305  cdlemk5u  41307  cdlemk12u  41318  cdlemk37  41360  cdlemk39  41362  cdlemkid1  41368  cdlemk51  41399  cdlemk52  41400  dia2dimlem1  41510  dia2dimlem2  41511  dia2dimlem3  41512  dia2dimlem10  41519  dia2dimlem12  41521  cdlemm10N  41564  cdlemn2  41641  cdlemn10  41652  dib2dim  41689  dih2dimb  41690  dih2dimbALTN  41691  dihjatcclem1  41864  dihjatcclem2  41865  dihjatcclem4  41867  dvh4dimat  41884