Theorem hlatjcl 39859

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 39855	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39781	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 39781	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18396	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	1, 4, 5, 7	syl3an 1166	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  (class class class)co 7356  Basecbs 17170  joincjn 18268  Latclat 18388  Atomscatm 39755  HLchlt 39842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-lat 18389  df-ats 39759  df-atl 39790  df-cvlat 39814  df-hlat 39843

This theorem is referenced by:  atcvr0eq  39918  2atjm  39937  atbtwn  39938  3dim0  39949  3dimlem3a  39952  3dimlem3OLDN  39954  3dimlem4OLDN  39957  3dim3  39961  2dim  39962  ps-1  39969  hlatexch3N  39972  hlatexch4  39973  ps-2b  39974  3atlem1  39975  3atlem2  39976  llni2  40004  llnle  40010  2at0mat0  40017  2atm  40019  islpln5  40027  lplni2  40029  lplnnle2at  40033  2atnelpln  40036  islpln2a  40040  llncvrlpln2  40049  2atmat  40053  2llnjaN  40058  islvol5  40071  lvoli2  40073  lvolnle3at  40074  3atnelvolN  40078  islvol2aN  40084  4atlem0a  40085  4atlem3  40088  4atlem3a  40089  4atlem3b  40090  4atlem4a  40091  4atlem4b  40092  4atlem4c  40093  4atlem4d  40094  4atlem9  40095  4atlem10a  40096  4atlem10  40098  4atlem11a  40099  4atlem11b  40100  4atlem11  40101  4atlem12a  40102  4atlem12b  40103  4atlem12  40104  4at  40105  4at2  40106  lplncvrlvol2  40107  2lplnja  40111  dalempjqeb  40137  dalemsjteb  40138  dalemtjueb  40139  dalemply  40146  dalem1  40151  dalemcea  40152  dalem3  40156  dalem4  40157  dalem5  40159  dalem-cly  40163  dalem17  40172  dalem21  40186  dalem24  40189  dalem25  40190  dalem27  40191  dalem38  40202  dalem39  40203  dalem43  40207  dalem44  40208  dalem45  40209  dalem55  40219  dalem56  40220  dalem57  40221  2atm2atN  40277  2llnma1b  40278  2llnma3r  40280  llnmod2i2  40355  llnexchb2lem  40360  dalawlem1  40363  dalawlem2  40364  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  dalawlem15  40377  lhp2lt  40493  lhpexle2lem  40501  lhpexle3lem  40503  lhp2at0  40524  lhp2atnle  40525  lhpat3  40538  4atexlempsb  40552  4atexlemqtb  40553  4atexlemunv  40558  4atexlemtlw  40559  4atexlemc  40561  4atexlemnclw  40562  4atexlemcnd  40564  trlval3  40679  trlval4  40680  cdlemc4  40686  cdlemc5  40687  cdlemc6  40688  cdlemd2  40691  cdleme0e  40709  cdlemeulpq  40712  cdleme01N  40713  cdleme0ex1N  40715  cdleme3g  40726  cdleme3h  40727  cdleme3  40729  cdleme4  40730  cdleme4a  40731  cdleme5  40732  cdleme7aa  40734  cdleme7c  40737  cdleme7d  40738  cdleme7e  40739  cdleme7ga  40740  cdleme7  40741  cdleme9b  40744  cdleme9  40745  cdleme10  40746  cdleme11c  40753  cdleme13  40764  cdleme15b  40767  cdleme15d  40769  cdleme15  40770  cdleme16b  40771  cdleme16e  40774  cdleme16f  40775  cdleme17b  40779  cdleme22gb  40786  cdlemedb  40789  cdlemednpq  40791  cdleme20zN  40793  cdleme19a  40795  cdleme19c  40797  cdleme20aN  40801  cdleme20c  40803  cdleme20d  40804  cdleme20e  40805  cdleme20j  40810  cdleme20l  40814  cdleme21c  40819  cdleme21ct  40821  cdleme22aa  40831  cdleme22b  40833  cdleme22cN  40834  cdleme22d  40835  cdleme22e  40836  cdleme22eALTN  40837  cdleme22f  40838  cdleme22g  40840  cdleme23a  40841  cdleme23b  40842  cdleme23c  40843  cdleme28a  40862  cdleme35a  40940  cdleme35fnpq  40941  cdleme35b  40942  cdleme35c  40943  cdleme35d  40944  cdleme35e  40945  cdleme35f  40946  cdleme42a  40963  cdleme42c  40964  cdleme42h  40974  cdleme42i  40975  cdlemeg46frv  41017  cdlemeg46vrg  41019  cdlemeg46rgv  41020  cdlemeg46req  41021  cdlemf1  41053  cdlemf2  41054  cdlemg2fv2  41092  cdlemg2m  41096  cdlemg4  41109  cdlemg8b  41120  cdlemg10bALTN  41128  cdlemg10c  41131  cdlemg10  41133  cdlemg12e  41139  cdlemg12f  41140  cdlemg12g  41141  cdlemg12  41142  cdlemg13a  41143  cdlemg17a  41153  cdlemg17dALTN  41156  cdlemg17h  41160  cdlemg17  41169  cdlemg18b  41171  cdlemg19a  41175  cdlemg19  41176  cdlemg27a  41184  cdlemg27b  41188  cdlemg31a  41189  cdlemg31b  41190  cdlemg33b0  41193  cdlemg33a  41198  trlcoabs2N  41214  trlcolem  41218  cdlemg42  41221  cdlemg46  41227  cdlemh1  41307  cdlemk3  41325  cdlemk10  41335  cdlemk12  41342  cdlemkole  41345  cdlemk14  41346  cdlemk15  41347  cdlemk1u  41351  cdlemk5u  41353  cdlemk12u  41364  cdlemk37  41406  cdlemk39  41408  cdlemkid1  41414  cdlemk51  41445  cdlemk52  41446  dia2dimlem1  41556  dia2dimlem2  41557  dia2dimlem3  41558  dia2dimlem10  41565  dia2dimlem12  41567  cdlemm10N  41610  cdlemn2  41687  cdlemn10  41698  dib2dim  41735  dih2dimb  41736  dih2dimbALTN  41737  dihjatcclem1  41910  dihjatcclem2  41911  dihjatcclem4  41913  dvh4dimat  41930