Theorem hlatjcl 29849

Description: Closure of join operation. Frequently-used special case of latjcl 14434 for atoms. (Contributed by NM, 15-Jun-2012.)

Hypotheses

Ref	Expression
hlatjcl.b	|- B = ( Base ` K )
hlatjcl.j	|- .\/ = ( join ` K )
hlatjcl.a	|- A = ( Atoms ` K )

Assertion

Ref	Expression
hlatjcl	|- ( ( K e. HL /\ X e. A /\ Y e. A ) -> ( X .\/ Y ) e. B )

Proof of Theorem hlatjcl

Step	Hyp	Ref	Expression
1		hllat 29846	. 2 |- ( K e. HL -> K e. Lat )
2		hlatjcl.b	. . 3 |- B = ( Base ` K )
3		hlatjcl.a	. . 3 |- A = ( Atoms ` K )
4	2, 3	atbase 29772	. 2 |- ( X e. A -> X e. B )
5	2, 3	atbase 29772	. 2 |- ( Y e. A -> Y e. B )
6		hlatjcl.j	. . 3 |- .\/ = ( join ` K )
7	2, 6	latjcl 14434	. 2 |- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
8	1, 4, 5, 7	syl3an 1226	1 |- ( ( K e. HL /\ X e. A /\ Y e. A ) -> ( X .\/ Y ) e. B )

Syntax hints:   -> wi 4   /\ w3a 936   = wceq 1649   e. wcel 1721   ` cfv 5413  (class class class)co 6040   Basecbs 13424   joincjn 14356   Latclat 14429   Atomscatm 29746   HLchlt 29833

This theorem is referenced by:  atcvr0eq  29908  2atjm  29927  atbtwn  29928  3dim0  29939  3dimlem3a  29942  3dimlem3OLDN  29944  3dimlem4OLDN  29947  3dim3  29951  2dim  29952  ps-1  29959  hlatexch3N  29962  hlatexch4  29963  ps-2b  29964  3atlem1  29965  3atlem2  29966  llni2  29994  llnle  30000  2at0mat0  30007  2atm  30009  islpln5  30017  lplni2  30019  lplnnle2at  30023  2atnelpln  30026  islpln2a  30030  llncvrlpln2  30039  2atmat  30043  2llnjaN  30048  islvol5  30061  lvoli2  30063  lvolnle3at  30064  3atnelvolN  30068  islvol2aN  30074  4atlem0a  30075  4atlem3  30078  4atlem3a  30079  4atlem3b  30080  4atlem4a  30081  4atlem4b  30082  4atlem4c  30083  4atlem4d  30084  4atlem9  30085  4atlem10a  30086  4atlem10  30088  4atlem11a  30089  4atlem11b  30090  4atlem11  30091  4atlem12a  30092  4atlem12b  30093  4atlem12  30094  4at  30095  4at2  30096  lplncvrlvol2  30097  2lplnja  30101  dalempjqeb  30127  dalemsjteb  30128  dalemtjueb  30129  dalemply  30136  dalem1  30141  dalemcea  30142  dalem3  30146  dalem4  30147  dalem5  30149  dalem-cly  30153  dalem17  30162  dalem21  30176  dalem24  30179  dalem25  30180  dalem27  30181  dalem38  30192  dalem39  30193  dalem43  30197  dalem44  30198  dalem45  30199  dalem55  30209  dalem56  30210  dalem57  30211  2atm2atN  30267  2llnma1b  30268  2llnma3r  30270  llnmod2i2  30345  llnexchb2lem  30350  dalawlem1  30353  dalawlem2  30354  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  dalawlem15  30367  lhp2lt  30483  lhpexle2lem  30491  lhpexle3lem  30493  lhp2at0  30514  lhp2atnle  30515  lhpat3  30528  4atexlempsb  30542  4atexlemqtb  30543  4atexlemunv  30548  4atexlemtlw  30549  4atexlemc  30551  4atexlemnclw  30552  4atexlemcnd  30554  trlval3  30669  trlval4  30670  cdlemc4  30676  cdlemc5  30677  cdlemc6  30678  cdlemd2  30681  cdleme0e  30699  cdlemeulpq  30702  cdleme01N  30703  cdleme0ex1N  30705  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme4  30720  cdleme4a  30721  cdleme5  30722  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme9b  30734  cdleme9  30735  cdleme10  30736  cdleme11c  30743  cdleme13  30754  cdleme15b  30757  cdleme15d  30759  cdleme15  30760  cdleme16b  30761  cdleme16e  30764  cdleme16f  30765  cdleme17b  30769  cdleme22gb  30776  cdlemedb  30779  cdlemednpq  30781  cdleme20zN  30783  cdleme20y  30784  cdleme19a  30785  cdleme19c  30787  cdleme20aN  30791  cdleme20c  30793  cdleme20d  30794  cdleme20e  30795  cdleme20j  30800  cdleme20l  30804  cdleme21c  30809  cdleme21ct  30811  cdleme22aa  30821  cdleme22b  30823  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f  30828  cdleme22g  30830  cdleme23a  30831  cdleme23b  30832  cdleme23c  30833  cdleme28a  30852  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme35e  30935  cdleme35f  30936  cdleme42a  30953  cdleme42c  30954  cdleme42h  30964  cdleme42i  30965  cdlemeg46frv  31007  cdlemeg46vrg  31009  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemf1  31043  cdlemf2  31044  cdlemg2fv2  31082  cdlemg2m  31086  cdlemg4  31099  cdlemg8b  31110  cdlemg10bALTN  31118  cdlemg10c  31121  cdlemg10  31123  cdlemg12e  31129  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg17a  31143  cdlemg17dALTN  31146  cdlemg17h  31150  cdlemg17  31159  cdlemg18b  31161  cdlemg19a  31165  cdlemg19  31166  cdlemg27a  31174  cdlemg27b  31178  cdlemg31a  31179  cdlemg31b  31180  cdlemg33b0  31183  cdlemg33a  31188  trlcoabs2N  31204  trlcolem  31208  cdlemg42  31211  cdlemg46  31217  cdlemh1  31297  cdlemk3  31315  cdlemk10  31325  cdlemk12  31332  cdlemkole  31335  cdlemk14  31336  cdlemk15  31337  cdlemk1u  31341  cdlemk5u  31343  cdlemk12u  31354  cdlemk37  31396  cdlemk39  31398  cdlemkid1  31404  cdlemk51  31435  cdlemk52  31436  dia2dimlem1  31547  dia2dimlem2  31548  dia2dimlem3  31549  dia2dimlem10  31556  dia2dimlem12  31558  cdlemm10N  31601  cdlemn2  31678  cdlemn10  31689  dib2dim  31726  dih2dimb  31727  dih2dimbALTN  31728  dihjatcclem1  31901  dihjatcclem2  31902  dihjatcclem4  31904  dvh4dimat  31921

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-ov 6043  df-lat 14430  df-ats 29750  df-atl 29781  df-cvlat 29805  df-hlat 29834