Theorem hlatjcl 37388

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  joincjn 18038  Latclat 18158  Atomscatm 37284  HLchlt 37371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-lub 18073  df-glb 18074  df-join 18075  df-meet 18076  df-lat 18159  df-ats 37288  df-atl 37319  df-cvlat 37343  df-hlat 37372

This theorem is referenced by:  atcvr0eq  37447  2atjm  37466  atbtwn  37467  3dim0  37478  3dimlem3a  37481  3dimlem3OLDN  37483  3dimlem4OLDN  37486  3dim3  37490  2dim  37491  ps-1  37498  hlatexch3N  37501  hlatexch4  37502  ps-2b  37503  3atlem1  37504  3atlem2  37505  llni2  37533  llnle  37539  2at0mat0  37546  2atm  37548  islpln5  37556  lplni2  37558  lplnnle2at  37562  2atnelpln  37565  islpln2a  37569  llncvrlpln2  37578  2atmat  37582  2llnjaN  37587  islvol5  37600  lvoli2  37602  lvolnle3at  37603  3atnelvolN  37607  islvol2aN  37613  4atlem0a  37614  4atlem3  37617  4atlem3a  37618  4atlem3b  37619  4atlem4a  37620  4atlem4b  37621  4atlem4c  37622  4atlem4d  37623  4atlem9  37624  4atlem10a  37625  4atlem10  37627  4atlem11a  37628  4atlem11b  37629  4atlem11  37630  4atlem12a  37631  4atlem12b  37632  4atlem12  37633  4at  37634  4at2  37635  lplncvrlvol2  37636  2lplnja  37640  dalempjqeb  37666  dalemsjteb  37667  dalemtjueb  37668  dalemply  37675  dalem1  37680  dalemcea  37681  dalem3  37685  dalem4  37686  dalem5  37688  dalem-cly  37692  dalem17  37701  dalem21  37715  dalem24  37718  dalem25  37719  dalem27  37720  dalem38  37731  dalem39  37732  dalem43  37736  dalem44  37737  dalem45  37738  dalem55  37748  dalem56  37749  dalem57  37750  2atm2atN  37806  2llnma1b  37807  2llnma3r  37809  llnmod2i2  37884  llnexchb2lem  37889  dalawlem1  37892  dalawlem2  37893  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  dalawlem15  37906  lhp2lt  38022  lhpexle2lem  38030  lhpexle3lem  38032  lhp2at0  38053  lhp2atnle  38054  lhpat3  38067  4atexlempsb  38081  4atexlemqtb  38082  4atexlemunv  38087  4atexlemtlw  38088  4atexlemc  38090  4atexlemnclw  38091  4atexlemcnd  38093  trlval3  38208  trlval4  38209  cdlemc4  38215  cdlemc5  38216  cdlemc6  38217  cdlemd2  38220  cdleme0e  38238  cdlemeulpq  38241  cdleme01N  38242  cdleme0ex1N  38244  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme4  38259  cdleme4a  38260  cdleme5  38261  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme9b  38273  cdleme9  38274  cdleme10  38275  cdleme11c  38282  cdleme13  38293  cdleme15b  38296  cdleme15d  38298  cdleme15  38299  cdleme16b  38300  cdleme16e  38303  cdleme16f  38304  cdleme17b  38308  cdleme22gb  38315  cdlemedb  38318  cdlemednpq  38320  cdleme20zN  38322  cdleme19a  38324  cdleme19c  38326  cdleme20aN  38330  cdleme20c  38332  cdleme20d  38333  cdleme20e  38334  cdleme20j  38339  cdleme20l  38343  cdleme21c  38348  cdleme21ct  38350  cdleme22aa  38360  cdleme22b  38362  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme22g  38369  cdleme23a  38370  cdleme23b  38371  cdleme23c  38372  cdleme28a  38391  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme35e  38474  cdleme35f  38475  cdleme42a  38492  cdleme42c  38493  cdleme42h  38503  cdleme42i  38504  cdlemeg46frv  38546  cdlemeg46vrg  38548  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemf1  38582  cdlemf2  38583  cdlemg2fv2  38621  cdlemg2m  38625  cdlemg4  38638  cdlemg8b  38649  cdlemg10bALTN  38657  cdlemg10c  38660  cdlemg10  38662  cdlemg12e  38668  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg17a  38682  cdlemg17dALTN  38685  cdlemg17h  38689  cdlemg17  38698  cdlemg18b  38700  cdlemg19a  38704  cdlemg19  38705  cdlemg27a  38713  cdlemg27b  38717  cdlemg31a  38718  cdlemg31b  38719  cdlemg33b0  38722  cdlemg33a  38727  trlcoabs2N  38743  trlcolem  38747  cdlemg42  38750  cdlemg46  38756  cdlemh1  38836  cdlemk3  38854  cdlemk10  38864  cdlemk12  38871  cdlemkole  38874  cdlemk14  38875  cdlemk15  38876  cdlemk1u  38880  cdlemk5u  38882  cdlemk12u  38893  cdlemk37  38935  cdlemk39  38937  cdlemkid1  38943  cdlemk51  38974  cdlemk52  38975  dia2dimlem1  39085  dia2dimlem2  39086  dia2dimlem3  39087  dia2dimlem10  39094  dia2dimlem12  39096  cdlemm10N  39139  cdlemn2  39216  cdlemn10  39227  dib2dim  39264  dih2dimb  39265  dih2dimbALTN  39266  dihjatcclem1  39439  dihjatcclem2  39440  dihjatcclem4  39442  dvh4dimat  39459