Theorem hlatjcl 39369

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6560  (class class class)co 7432  Basecbs 17248  joincjn 18358  Latclat 18477  Atomscatm 39265  HLchlt 39352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-lub 18392  df-glb 18393  df-join 18394  df-meet 18395  df-lat 18478  df-ats 39269  df-atl 39300  df-cvlat 39324  df-hlat 39353

This theorem is referenced by:  atcvr0eq  39429  2atjm  39448  atbtwn  39449  3dim0  39460  3dimlem3a  39463  3dimlem3OLDN  39465  3dimlem4OLDN  39468  3dim3  39472  2dim  39473  ps-1  39480  hlatexch3N  39483  hlatexch4  39484  ps-2b  39485  3atlem1  39486  3atlem2  39487  llni2  39515  llnle  39521  2at0mat0  39528  2atm  39530  islpln5  39538  lplni2  39540  lplnnle2at  39544  2atnelpln  39547  islpln2a  39551  llncvrlpln2  39560  2atmat  39564  2llnjaN  39569  islvol5  39582  lvoli2  39584  lvolnle3at  39585  3atnelvolN  39589  islvol2aN  39595  4atlem0a  39596  4atlem3  39599  4atlem3a  39600  4atlem3b  39601  4atlem4a  39602  4atlem4b  39603  4atlem4c  39604  4atlem4d  39605  4atlem9  39606  4atlem10a  39607  4atlem10  39609  4atlem11a  39610  4atlem11b  39611  4atlem11  39612  4atlem12a  39613  4atlem12b  39614  4atlem12  39615  4at  39616  4at2  39617  lplncvrlvol2  39618  2lplnja  39622  dalempjqeb  39648  dalemsjteb  39649  dalemtjueb  39650  dalemply  39657  dalem1  39662  dalemcea  39663  dalem3  39667  dalem4  39668  dalem5  39670  dalem-cly  39674  dalem17  39683  dalem21  39697  dalem24  39700  dalem25  39701  dalem27  39702  dalem38  39713  dalem39  39714  dalem43  39718  dalem44  39719  dalem45  39720  dalem55  39730  dalem56  39731  dalem57  39732  2atm2atN  39788  2llnma1b  39789  2llnma3r  39791  llnmod2i2  39866  llnexchb2lem  39871  dalawlem1  39874  dalawlem2  39875  dalawlem3  39876  dalawlem4  39877  dalawlem5  39878  dalawlem6  39879  dalawlem7  39880  dalawlem8  39881  dalawlem9  39882  dalawlem11  39884  dalawlem12  39885  dalawlem15  39888  lhp2lt  40004  lhpexle2lem  40012  lhpexle3lem  40014  lhp2at0  40035  lhp2atnle  40036  lhpat3  40049  4atexlempsb  40063  4atexlemqtb  40064  4atexlemunv  40069  4atexlemtlw  40070  4atexlemc  40072  4atexlemnclw  40073  4atexlemcnd  40075  trlval3  40190  trlval4  40191  cdlemc4  40197  cdlemc5  40198  cdlemc6  40199  cdlemd2  40202  cdleme0e  40220  cdlemeulpq  40223  cdleme01N  40224  cdleme0ex1N  40226  cdleme3g  40237  cdleme3h  40238  cdleme3  40240  cdleme4  40241  cdleme4a  40242  cdleme5  40243  cdleme7aa  40245  cdleme7c  40248  cdleme7d  40249  cdleme7e  40250  cdleme7ga  40251  cdleme7  40252  cdleme9b  40255  cdleme9  40256  cdleme10  40257  cdleme11c  40264  cdleme13  40275  cdleme15b  40278  cdleme15d  40280  cdleme15  40281  cdleme16b  40282  cdleme16e  40285  cdleme16f  40286  cdleme17b  40290  cdleme22gb  40297  cdlemedb  40300  cdlemednpq  40302  cdleme20zN  40304  cdleme19a  40306  cdleme19c  40308  cdleme20aN  40312  cdleme20c  40314  cdleme20d  40315  cdleme20e  40316  cdleme20j  40321  cdleme20l  40325  cdleme21c  40330  cdleme21ct  40332  cdleme22aa  40342  cdleme22b  40344  cdleme22cN  40345  cdleme22d  40346  cdleme22e  40347  cdleme22eALTN  40348  cdleme22f  40349  cdleme22g  40351  cdleme23a  40352  cdleme23b  40353  cdleme23c  40354  cdleme28a  40373  cdleme35a  40451  cdleme35fnpq  40452  cdleme35b  40453  cdleme35c  40454  cdleme35d  40455  cdleme35e  40456  cdleme35f  40457  cdleme42a  40474  cdleme42c  40475  cdleme42h  40485  cdleme42i  40486  cdlemeg46frv  40528  cdlemeg46vrg  40530  cdlemeg46rgv  40531  cdlemeg46req  40532  cdlemf1  40564  cdlemf2  40565  cdlemg2fv2  40603  cdlemg2m  40607  cdlemg4  40620  cdlemg8b  40631  cdlemg10bALTN  40639  cdlemg10c  40642  cdlemg10  40644  cdlemg12e  40650  cdlemg12f  40651  cdlemg12g  40652  cdlemg12  40653  cdlemg13a  40654  cdlemg17a  40664  cdlemg17dALTN  40667  cdlemg17h  40671  cdlemg17  40680  cdlemg18b  40682  cdlemg19a  40686  cdlemg19  40687  cdlemg27a  40695  cdlemg27b  40699  cdlemg31a  40700  cdlemg31b  40701  cdlemg33b0  40704  cdlemg33a  40709  trlcoabs2N  40725  trlcolem  40729  cdlemg42  40732  cdlemg46  40738  cdlemh1  40818  cdlemk3  40836  cdlemk10  40846  cdlemk12  40853  cdlemkole  40856  cdlemk14  40857  cdlemk15  40858  cdlemk1u  40862  cdlemk5u  40864  cdlemk12u  40875  cdlemk37  40917  cdlemk39  40919  cdlemkid1  40925  cdlemk51  40956  cdlemk52  40957  dia2dimlem1  41067  dia2dimlem2  41068  dia2dimlem3  41069  dia2dimlem10  41076  dia2dimlem12  41078  cdlemm10N  41121  cdlemn2  41198  cdlemn10  41209  dib2dim  41246  dih2dimb  41247  dih2dimbALTN  41248  dihjatcclem1  41421  dihjatcclem2  41422  dihjatcclem4  41424  dvh4dimat  41441