Theorem hlatjcl 36663

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ‘cfv 6324  (class class class)co 7135  Basecbs 16475  joincjn 17546  Latclat 17647  Atomscatm 36559  HLchlt 36646

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-lub 17576  df-glb 17577  df-join 17578  df-meet 17579  df-lat 17648  df-ats 36563  df-atl 36594  df-cvlat 36618  df-hlat 36647

This theorem is referenced by:  atcvr0eq  36722  2atjm  36741  atbtwn  36742  3dim0  36753  3dimlem3a  36756  3dimlem3OLDN  36758  3dimlem4OLDN  36761  3dim3  36765  2dim  36766  ps-1  36773  hlatexch3N  36776  hlatexch4  36777  ps-2b  36778  3atlem1  36779  3atlem2  36780  llni2  36808  llnle  36814  2at0mat0  36821  2atm  36823  islpln5  36831  lplni2  36833  lplnnle2at  36837  2atnelpln  36840  islpln2a  36844  llncvrlpln2  36853  2atmat  36857  2llnjaN  36862  islvol5  36875  lvoli2  36877  lvolnle3at  36878  3atnelvolN  36882  islvol2aN  36888  4atlem0a  36889  4atlem3  36892  4atlem3a  36893  4atlem3b  36894  4atlem4a  36895  4atlem4b  36896  4atlem4c  36897  4atlem4d  36898  4atlem9  36899  4atlem10a  36900  4atlem10  36902  4atlem11a  36903  4atlem11b  36904  4atlem11  36905  4atlem12a  36906  4atlem12b  36907  4atlem12  36908  4at  36909  4at2  36910  lplncvrlvol2  36911  2lplnja  36915  dalempjqeb  36941  dalemsjteb  36942  dalemtjueb  36943  dalemply  36950  dalem1  36955  dalemcea  36956  dalem3  36960  dalem4  36961  dalem5  36963  dalem-cly  36967  dalem17  36976  dalem21  36990  dalem24  36993  dalem25  36994  dalem27  36995  dalem38  37006  dalem39  37007  dalem43  37011  dalem44  37012  dalem45  37013  dalem55  37023  dalem56  37024  dalem57  37025  2atm2atN  37081  2llnma1b  37082  2llnma3r  37084  llnmod2i2  37159  llnexchb2lem  37164  dalawlem1  37167  dalawlem2  37168  dalawlem3  37169  dalawlem4  37170  dalawlem5  37171  dalawlem6  37172  dalawlem7  37173  dalawlem8  37174  dalawlem9  37175  dalawlem11  37177  dalawlem12  37178  dalawlem15  37181  lhp2lt  37297  lhpexle2lem  37305  lhpexle3lem  37307  lhp2at0  37328  lhp2atnle  37329  lhpat3  37342  4atexlempsb  37356  4atexlemqtb  37357  4atexlemunv  37362  4atexlemtlw  37363  4atexlemc  37365  4atexlemnclw  37366  4atexlemcnd  37368  trlval3  37483  trlval4  37484  cdlemc4  37490  cdlemc5  37491  cdlemc6  37492  cdlemd2  37495  cdleme0e  37513  cdlemeulpq  37516  cdleme01N  37517  cdleme0ex1N  37519  cdleme3g  37530  cdleme3h  37531  cdleme3  37533  cdleme4  37534  cdleme4a  37535  cdleme5  37536  cdleme7aa  37538  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme9b  37548  cdleme9  37549  cdleme10  37550  cdleme11c  37557  cdleme13  37568  cdleme15b  37571  cdleme15d  37573  cdleme15  37574  cdleme16b  37575  cdleme16e  37578  cdleme16f  37579  cdleme17b  37583  cdleme22gb  37590  cdlemedb  37593  cdlemednpq  37595  cdleme20zN  37597  cdleme19a  37599  cdleme19c  37601  cdleme20aN  37605  cdleme20c  37607  cdleme20d  37608  cdleme20e  37609  cdleme20j  37614  cdleme20l  37618  cdleme21c  37623  cdleme21ct  37625  cdleme22aa  37635  cdleme22b  37637  cdleme22cN  37638  cdleme22d  37639  cdleme22e  37640  cdleme22eALTN  37641  cdleme22f  37642  cdleme22g  37644  cdleme23a  37645  cdleme23b  37646  cdleme23c  37647  cdleme28a  37666  cdleme35a  37744  cdleme35fnpq  37745  cdleme35b  37746  cdleme35c  37747  cdleme35d  37748  cdleme35e  37749  cdleme35f  37750  cdleme42a  37767  cdleme42c  37768  cdleme42h  37778  cdleme42i  37779  cdlemeg46frv  37821  cdlemeg46vrg  37823  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemf1  37857  cdlemf2  37858  cdlemg2fv2  37896  cdlemg2m  37900  cdlemg4  37913  cdlemg8b  37924  cdlemg10bALTN  37932  cdlemg10c  37935  cdlemg10  37937  cdlemg12e  37943  cdlemg12f  37944  cdlemg12g  37945  cdlemg12  37946  cdlemg13a  37947  cdlemg17a  37957  cdlemg17dALTN  37960  cdlemg17h  37964  cdlemg17  37973  cdlemg18b  37975  cdlemg19a  37979  cdlemg19  37980  cdlemg27a  37988  cdlemg27b  37992  cdlemg31a  37993  cdlemg31b  37994  cdlemg33b0  37997  cdlemg33a  38002  trlcoabs2N  38018  trlcolem  38022  cdlemg42  38025  cdlemg46  38031  cdlemh1  38111  cdlemk3  38129  cdlemk10  38139  cdlemk12  38146  cdlemkole  38149  cdlemk14  38150  cdlemk15  38151  cdlemk1u  38155  cdlemk5u  38157  cdlemk12u  38168  cdlemk37  38210  cdlemk39  38212  cdlemkid1  38218  cdlemk51  38249  cdlemk52  38250  dia2dimlem1  38360  dia2dimlem2  38361  dia2dimlem3  38362  dia2dimlem10  38369  dia2dimlem12  38371  cdlemm10N  38414  cdlemn2  38491  cdlemn10  38502  dib2dim  38539  dih2dimb  38540  dih2dimbALTN  38541  dihjatcclem1  38714  dihjatcclem2  38715  dihjatcclem4  38717  dvh4dimat  38734