Theorem hlatjcl 38731

Description: Closure of join operation. Frequently-used special case of latjcl 18396 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 38727	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 38653	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 38653	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18396	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	1, 4, 5, 7	syl3an 1157	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ‘cfv 6534  (class class class)co 7402  Basecbs 17145  joincjn 18268  Latclat 18388  Atomscatm 38627  HLchlt 38714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-lat 18389  df-ats 38631  df-atl 38662  df-cvlat 38686  df-hlat 38715

This theorem is referenced by:  atcvr0eq  38791  2atjm  38810  atbtwn  38811  3dim0  38822  3dimlem3a  38825  3dimlem3OLDN  38827  3dimlem4OLDN  38830  3dim3  38834  2dim  38835  ps-1  38842  hlatexch3N  38845  hlatexch4  38846  ps-2b  38847  3atlem1  38848  3atlem2  38849  llni2  38877  llnle  38883  2at0mat0  38890  2atm  38892  islpln5  38900  lplni2  38902  lplnnle2at  38906  2atnelpln  38909  islpln2a  38913  llncvrlpln2  38922  2atmat  38926  2llnjaN  38931  islvol5  38944  lvoli2  38946  lvolnle3at  38947  3atnelvolN  38951  islvol2aN  38957  4atlem0a  38958  4atlem3  38961  4atlem3a  38962  4atlem3b  38963  4atlem4a  38964  4atlem4b  38965  4atlem4c  38966  4atlem4d  38967  4atlem9  38968  4atlem10a  38969  4atlem10  38971  4atlem11a  38972  4atlem11b  38973  4atlem11  38974  4atlem12a  38975  4atlem12b  38976  4atlem12  38977  4at  38978  4at2  38979  lplncvrlvol2  38980  2lplnja  38984  dalempjqeb  39010  dalemsjteb  39011  dalemtjueb  39012  dalemply  39019  dalem1  39024  dalemcea  39025  dalem3  39029  dalem4  39030  dalem5  39032  dalem-cly  39036  dalem17  39045  dalem21  39059  dalem24  39062  dalem25  39063  dalem27  39064  dalem38  39075  dalem39  39076  dalem43  39080  dalem44  39081  dalem45  39082  dalem55  39092  dalem56  39093  dalem57  39094  2atm2atN  39150  2llnma1b  39151  2llnma3r  39153  llnmod2i2  39228  llnexchb2lem  39233  dalawlem1  39236  dalawlem2  39237  dalawlem3  39238  dalawlem4  39239  dalawlem5  39240  dalawlem6  39241  dalawlem7  39242  dalawlem8  39243  dalawlem9  39244  dalawlem11  39246  dalawlem12  39247  dalawlem15  39250  lhp2lt  39366  lhpexle2lem  39374  lhpexle3lem  39376  lhp2at0  39397  lhp2atnle  39398  lhpat3  39411  4atexlempsb  39425  4atexlemqtb  39426  4atexlemunv  39431  4atexlemtlw  39432  4atexlemc  39434  4atexlemnclw  39435  4atexlemcnd  39437  trlval3  39552  trlval4  39553  cdlemc4  39559  cdlemc5  39560  cdlemc6  39561  cdlemd2  39564  cdleme0e  39582  cdlemeulpq  39585  cdleme01N  39586  cdleme0ex1N  39588  cdleme3g  39599  cdleme3h  39600  cdleme3  39602  cdleme4  39603  cdleme4a  39604  cdleme5  39605  cdleme7aa  39607  cdleme7c  39610  cdleme7d  39611  cdleme7e  39612  cdleme7ga  39613  cdleme7  39614  cdleme9b  39617  cdleme9  39618  cdleme10  39619  cdleme11c  39626  cdleme13  39637  cdleme15b  39640  cdleme15d  39642  cdleme15  39643  cdleme16b  39644  cdleme16e  39647  cdleme16f  39648  cdleme17b  39652  cdleme22gb  39659  cdlemedb  39662  cdlemednpq  39664  cdleme20zN  39666  cdleme19a  39668  cdleme19c  39670  cdleme20aN  39674  cdleme20c  39676  cdleme20d  39677  cdleme20e  39678  cdleme20j  39683  cdleme20l  39687  cdleme21c  39692  cdleme21ct  39694  cdleme22aa  39704  cdleme22b  39706  cdleme22cN  39707  cdleme22d  39708  cdleme22e  39709  cdleme22eALTN  39710  cdleme22f  39711  cdleme22g  39713  cdleme23a  39714  cdleme23b  39715  cdleme23c  39716  cdleme28a  39735  cdleme35a  39813  cdleme35fnpq  39814  cdleme35b  39815  cdleme35c  39816  cdleme35d  39817  cdleme35e  39818  cdleme35f  39819  cdleme42a  39836  cdleme42c  39837  cdleme42h  39847  cdleme42i  39848  cdlemeg46frv  39890  cdlemeg46vrg  39892  cdlemeg46rgv  39893  cdlemeg46req  39894  cdlemf1  39926  cdlemf2  39927  cdlemg2fv2  39965  cdlemg2m  39969  cdlemg4  39982  cdlemg8b  39993  cdlemg10bALTN  40001  cdlemg10c  40004  cdlemg10  40006  cdlemg12e  40012  cdlemg12f  40013  cdlemg12g  40014  cdlemg12  40015  cdlemg13a  40016  cdlemg17a  40026  cdlemg17dALTN  40029  cdlemg17h  40033  cdlemg17  40042  cdlemg18b  40044  cdlemg19a  40048  cdlemg19  40049  cdlemg27a  40057  cdlemg27b  40061  cdlemg31a  40062  cdlemg31b  40063  cdlemg33b0  40066  cdlemg33a  40071  trlcoabs2N  40087  trlcolem  40091  cdlemg42  40094  cdlemg46  40100  cdlemh1  40180  cdlemk3  40198  cdlemk10  40208  cdlemk12  40215  cdlemkole  40218  cdlemk14  40219  cdlemk15  40220  cdlemk1u  40224  cdlemk5u  40226  cdlemk12u  40237  cdlemk37  40279  cdlemk39  40281  cdlemkid1  40287  cdlemk51  40318  cdlemk52  40319  dia2dimlem1  40429  dia2dimlem2  40430  dia2dimlem3  40431  dia2dimlem10  40438  dia2dimlem12  40440  cdlemm10N  40483  cdlemn2  40560  cdlemn10  40571  dib2dim  40608  dih2dimb  40609  dih2dimbALTN  40610  dihjatcclem1  40783  dihjatcclem2  40784  dihjatcclem4  40786  dvh4dimat  40803