Theorem hlatjcl 39637

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  joincjn 18234  Latclat 18354  Atomscatm 39533  HLchlt 39620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-lub 18267  df-glb 18268  df-join 18269  df-meet 18270  df-lat 18355  df-ats 39537  df-atl 39568  df-cvlat 39592  df-hlat 39621

This theorem is referenced by:  atcvr0eq  39696  2atjm  39715  atbtwn  39716  3dim0  39727  3dimlem3a  39730  3dimlem3OLDN  39732  3dimlem4OLDN  39735  3dim3  39739  2dim  39740  ps-1  39747  hlatexch3N  39750  hlatexch4  39751  ps-2b  39752  3atlem1  39753  3atlem2  39754  llni2  39782  llnle  39788  2at0mat0  39795  2atm  39797  islpln5  39805  lplni2  39807  lplnnle2at  39811  2atnelpln  39814  islpln2a  39818  llncvrlpln2  39827  2atmat  39831  2llnjaN  39836  islvol5  39849  lvoli2  39851  lvolnle3at  39852  3atnelvolN  39856  islvol2aN  39862  4atlem0a  39863  4atlem3  39866  4atlem3a  39867  4atlem3b  39868  4atlem4a  39869  4atlem4b  39870  4atlem4c  39871  4atlem4d  39872  4atlem9  39873  4atlem10a  39874  4atlem10  39876  4atlem11a  39877  4atlem11b  39878  4atlem11  39879  4atlem12a  39880  4atlem12b  39881  4atlem12  39882  4at  39883  4at2  39884  lplncvrlvol2  39885  2lplnja  39889  dalempjqeb  39915  dalemsjteb  39916  dalemtjueb  39917  dalemply  39924  dalem1  39929  dalemcea  39930  dalem3  39934  dalem4  39935  dalem5  39937  dalem-cly  39941  dalem17  39950  dalem21  39964  dalem24  39967  dalem25  39968  dalem27  39969  dalem38  39980  dalem39  39981  dalem43  39985  dalem44  39986  dalem45  39987  dalem55  39997  dalem56  39998  dalem57  39999  2atm2atN  40055  2llnma1b  40056  2llnma3r  40058  llnmod2i2  40133  llnexchb2lem  40138  dalawlem1  40141  dalawlem2  40142  dalawlem3  40143  dalawlem4  40144  dalawlem5  40145  dalawlem6  40146  dalawlem7  40147  dalawlem8  40148  dalawlem9  40149  dalawlem11  40151  dalawlem12  40152  dalawlem15  40155  lhp2lt  40271  lhpexle2lem  40279  lhpexle3lem  40281  lhp2at0  40302  lhp2atnle  40303  lhpat3  40316  4atexlempsb  40330  4atexlemqtb  40331  4atexlemunv  40336  4atexlemtlw  40337  4atexlemc  40339  4atexlemnclw  40340  4atexlemcnd  40342  trlval3  40457  trlval4  40458  cdlemc4  40464  cdlemc5  40465  cdlemc6  40466  cdlemd2  40469  cdleme0e  40487  cdlemeulpq  40490  cdleme01N  40491  cdleme0ex1N  40493  cdleme3g  40504  cdleme3h  40505  cdleme3  40507  cdleme4  40508  cdleme4a  40509  cdleme5  40510  cdleme7aa  40512  cdleme7c  40515  cdleme7d  40516  cdleme7e  40517  cdleme7ga  40518  cdleme7  40519  cdleme9b  40522  cdleme9  40523  cdleme10  40524  cdleme11c  40531  cdleme13  40542  cdleme15b  40545  cdleme15d  40547  cdleme15  40548  cdleme16b  40549  cdleme16e  40552  cdleme16f  40553  cdleme17b  40557  cdleme22gb  40564  cdlemedb  40567  cdlemednpq  40569  cdleme20zN  40571  cdleme19a  40573  cdleme19c  40575  cdleme20aN  40579  cdleme20c  40581  cdleme20d  40582  cdleme20e  40583  cdleme20j  40588  cdleme20l  40592  cdleme21c  40597  cdleme21ct  40599  cdleme22aa  40609  cdleme22b  40611  cdleme22cN  40612  cdleme22d  40613  cdleme22e  40614  cdleme22eALTN  40615  cdleme22f  40616  cdleme22g  40618  cdleme23a  40619  cdleme23b  40620  cdleme23c  40621  cdleme28a  40640  cdleme35a  40718  cdleme35fnpq  40719  cdleme35b  40720  cdleme35c  40721  cdleme35d  40722  cdleme35e  40723  cdleme35f  40724  cdleme42a  40741  cdleme42c  40742  cdleme42h  40752  cdleme42i  40753  cdlemeg46frv  40795  cdlemeg46vrg  40797  cdlemeg46rgv  40798  cdlemeg46req  40799  cdlemf1  40831  cdlemf2  40832  cdlemg2fv2  40870  cdlemg2m  40874  cdlemg4  40887  cdlemg8b  40898  cdlemg10bALTN  40906  cdlemg10c  40909  cdlemg10  40911  cdlemg12e  40917  cdlemg12f  40918  cdlemg12g  40919  cdlemg12  40920  cdlemg13a  40921  cdlemg17a  40931  cdlemg17dALTN  40934  cdlemg17h  40938  cdlemg17  40947  cdlemg18b  40949  cdlemg19a  40953  cdlemg19  40954  cdlemg27a  40962  cdlemg27b  40966  cdlemg31a  40967  cdlemg31b  40968  cdlemg33b0  40971  cdlemg33a  40976  trlcoabs2N  40992  trlcolem  40996  cdlemg42  40999  cdlemg46  41005  cdlemh1  41085  cdlemk3  41103  cdlemk10  41113  cdlemk12  41120  cdlemkole  41123  cdlemk14  41124  cdlemk15  41125  cdlemk1u  41129  cdlemk5u  41131  cdlemk12u  41142  cdlemk37  41184  cdlemk39  41186  cdlemkid1  41192  cdlemk51  41223  cdlemk52  41224  dia2dimlem1  41334  dia2dimlem2  41335  dia2dimlem3  41336  dia2dimlem10  41343  dia2dimlem12  41345  cdlemm10N  41388  cdlemn2  41465  cdlemn10  41476  dib2dim  41513  dih2dimb  41514  dih2dimbALTN  41515  dihjatcclem1  41688  dihjatcclem2  41689  dihjatcclem4  41691  dvh4dimat  41708