Theorem hlatjcl 37004

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  ‘cfv 6339  (class class class)co 7170  Basecbs 16586  joincjn 17670  Latclat 17771  Atomscatm 36900  HLchlt 36987

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-lub 17700  df-glb 17701  df-join 17702  df-meet 17703  df-lat 17772  df-ats 36904  df-atl 36935  df-cvlat 36959  df-hlat 36988

This theorem is referenced by:  atcvr0eq  37063  2atjm  37082  atbtwn  37083  3dim0  37094  3dimlem3a  37097  3dimlem3OLDN  37099  3dimlem4OLDN  37102  3dim3  37106  2dim  37107  ps-1  37114  hlatexch3N  37117  hlatexch4  37118  ps-2b  37119  3atlem1  37120  3atlem2  37121  llni2  37149  llnle  37155  2at0mat0  37162  2atm  37164  islpln5  37172  lplni2  37174  lplnnle2at  37178  2atnelpln  37181  islpln2a  37185  llncvrlpln2  37194  2atmat  37198  2llnjaN  37203  islvol5  37216  lvoli2  37218  lvolnle3at  37219  3atnelvolN  37223  islvol2aN  37229  4atlem0a  37230  4atlem3  37233  4atlem3a  37234  4atlem3b  37235  4atlem4a  37236  4atlem4b  37237  4atlem4c  37238  4atlem4d  37239  4atlem9  37240  4atlem10a  37241  4atlem10  37243  4atlem11a  37244  4atlem11b  37245  4atlem11  37246  4atlem12a  37247  4atlem12b  37248  4atlem12  37249  4at  37250  4at2  37251  lplncvrlvol2  37252  2lplnja  37256  dalempjqeb  37282  dalemsjteb  37283  dalemtjueb  37284  dalemply  37291  dalem1  37296  dalemcea  37297  dalem3  37301  dalem4  37302  dalem5  37304  dalem-cly  37308  dalem17  37317  dalem21  37331  dalem24  37334  dalem25  37335  dalem27  37336  dalem38  37347  dalem39  37348  dalem43  37352  dalem44  37353  dalem45  37354  dalem55  37364  dalem56  37365  dalem57  37366  2atm2atN  37422  2llnma1b  37423  2llnma3r  37425  llnmod2i2  37500  llnexchb2lem  37505  dalawlem1  37508  dalawlem2  37509  dalawlem3  37510  dalawlem4  37511  dalawlem5  37512  dalawlem6  37513  dalawlem7  37514  dalawlem8  37515  dalawlem9  37516  dalawlem11  37518  dalawlem12  37519  dalawlem15  37522  lhp2lt  37638  lhpexle2lem  37646  lhpexle3lem  37648  lhp2at0  37669  lhp2atnle  37670  lhpat3  37683  4atexlempsb  37697  4atexlemqtb  37698  4atexlemunv  37703  4atexlemtlw  37704  4atexlemc  37706  4atexlemnclw  37707  4atexlemcnd  37709  trlval3  37824  trlval4  37825  cdlemc4  37831  cdlemc5  37832  cdlemc6  37833  cdlemd2  37836  cdleme0e  37854  cdlemeulpq  37857  cdleme01N  37858  cdleme0ex1N  37860  cdleme3g  37871  cdleme3h  37872  cdleme3  37874  cdleme4  37875  cdleme4a  37876  cdleme5  37877  cdleme7aa  37879  cdleme7c  37882  cdleme7d  37883  cdleme7e  37884  cdleme7ga  37885  cdleme7  37886  cdleme9b  37889  cdleme9  37890  cdleme10  37891  cdleme11c  37898  cdleme13  37909  cdleme15b  37912  cdleme15d  37914  cdleme15  37915  cdleme16b  37916  cdleme16e  37919  cdleme16f  37920  cdleme17b  37924  cdleme22gb  37931  cdlemedb  37934  cdlemednpq  37936  cdleme20zN  37938  cdleme19a  37940  cdleme19c  37942  cdleme20aN  37946  cdleme20c  37948  cdleme20d  37949  cdleme20e  37950  cdleme20j  37955  cdleme20l  37959  cdleme21c  37964  cdleme21ct  37966  cdleme22aa  37976  cdleme22b  37978  cdleme22cN  37979  cdleme22d  37980  cdleme22e  37981  cdleme22eALTN  37982  cdleme22f  37983  cdleme22g  37985  cdleme23a  37986  cdleme23b  37987  cdleme23c  37988  cdleme28a  38007  cdleme35a  38085  cdleme35fnpq  38086  cdleme35b  38087  cdleme35c  38088  cdleme35d  38089  cdleme35e  38090  cdleme35f  38091  cdleme42a  38108  cdleme42c  38109  cdleme42h  38119  cdleme42i  38120  cdlemeg46frv  38162  cdlemeg46vrg  38164  cdlemeg46rgv  38165  cdlemeg46req  38166  cdlemf1  38198  cdlemf2  38199  cdlemg2fv2  38237  cdlemg2m  38241  cdlemg4  38254  cdlemg8b  38265  cdlemg10bALTN  38273  cdlemg10c  38276  cdlemg10  38278  cdlemg12e  38284  cdlemg12f  38285  cdlemg12g  38286  cdlemg12  38287  cdlemg13a  38288  cdlemg17a  38298  cdlemg17dALTN  38301  cdlemg17h  38305  cdlemg17  38314  cdlemg18b  38316  cdlemg19a  38320  cdlemg19  38321  cdlemg27a  38329  cdlemg27b  38333  cdlemg31a  38334  cdlemg31b  38335  cdlemg33b0  38338  cdlemg33a  38343  trlcoabs2N  38359  trlcolem  38363  cdlemg42  38366  cdlemg46  38372  cdlemh1  38452  cdlemk3  38470  cdlemk10  38480  cdlemk12  38487  cdlemkole  38490  cdlemk14  38491  cdlemk15  38492  cdlemk1u  38496  cdlemk5u  38498  cdlemk12u  38509  cdlemk37  38551  cdlemk39  38553  cdlemkid1  38559  cdlemk51  38590  cdlemk52  38591  dia2dimlem1  38701  dia2dimlem2  38702  dia2dimlem3  38703  dia2dimlem10  38710  dia2dimlem12  38712  cdlemm10N  38755  cdlemn2  38832  cdlemn10  38843  dib2dim  38880  dih2dimb  38881  dih2dimbALTN  38882  dihjatcclem1  39055  dihjatcclem2  39056  dihjatcclem4  39058  dvh4dimat  39075