Theorem hlatjcl 32932

Description: Closure of join operation. Frequently-used special case of latjcl 16297 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 32929	. 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 32855	. 2 |- ( X e. A -> X e. B )
5	2, 3	atbase 32855	. 2 |- ( Y e. A -> Y e. B )
6		hlatjcl.j	. . 3 |- .\/ = ( join ` K )
7	2, 6	latjcl 16297	. 2 |- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
8	1, 4, 5, 7	syl3an 1310	1 |- ( ( K e. HL /\ X e. A /\ Y e. A ) -> ( X .\/ Y ) e. B )

Syntax hints:   -> wi 4   /\ w3a 985   = wceq 1444   e. wcel 1887   ` cfv 5582  (class class class)co 6290   Basecbs 15121   joincjn 16189   Latclat 16291   Atomscatm 32829   HLchlt 32916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-lub 16220  df-glb 16221  df-join 16222  df-meet 16223  df-lat 16292  df-ats 32833  df-atl 32864  df-cvlat 32888  df-hlat 32917

This theorem is referenced by:  atcvr0eq  32991  2atjm  33010  atbtwn  33011  3dim0  33022  3dimlem3a  33025  3dimlem3OLDN  33027  3dimlem4OLDN  33030  3dim3  33034  2dim  33035  ps-1  33042  hlatexch3N  33045  hlatexch4  33046  ps-2b  33047  3atlem1  33048  3atlem2  33049  llni2  33077  llnle  33083  2at0mat0  33090  2atm  33092  islpln5  33100  lplni2  33102  lplnnle2at  33106  2atnelpln  33109  islpln2a  33113  llncvrlpln2  33122  2atmat  33126  2llnjaN  33131  islvol5  33144  lvoli2  33146  lvolnle3at  33147  3atnelvolN  33151  islvol2aN  33157  4atlem0a  33158  4atlem3  33161  4atlem3a  33162  4atlem3b  33163  4atlem4a  33164  4atlem4b  33165  4atlem4c  33166  4atlem4d  33167  4atlem9  33168  4atlem10a  33169  4atlem10  33171  4atlem11a  33172  4atlem11b  33173  4atlem11  33174  4atlem12a  33175  4atlem12b  33176  4atlem12  33177  4at  33178  4at2  33179  lplncvrlvol2  33180  2lplnja  33184  dalempjqeb  33210  dalemsjteb  33211  dalemtjueb  33212  dalemply  33219  dalem1  33224  dalemcea  33225  dalem3  33229  dalem4  33230  dalem5  33232  dalem-cly  33236  dalem17  33245  dalem21  33259  dalem24  33262  dalem25  33263  dalem27  33264  dalem38  33275  dalem39  33276  dalem43  33280  dalem44  33281  dalem45  33282  dalem55  33292  dalem56  33293  dalem57  33294  2atm2atN  33350  2llnma1b  33351  2llnma3r  33353  llnmod2i2  33428  llnexchb2lem  33433  dalawlem1  33436  dalawlem2  33437  dalawlem3  33438  dalawlem4  33439  dalawlem5  33440  dalawlem6  33441  dalawlem7  33442  dalawlem8  33443  dalawlem9  33444  dalawlem11  33446  dalawlem12  33447  dalawlem15  33450  lhp2lt  33566  lhpexle2lem  33574  lhpexle3lem  33576  lhp2at0  33597  lhp2atnle  33598  lhpat3  33611  4atexlempsb  33625  4atexlemqtb  33626  4atexlemunv  33631  4atexlemtlw  33632  4atexlemc  33634  4atexlemnclw  33635  4atexlemcnd  33637  trlval3  33753  trlval4  33754  cdlemc4  33760  cdlemc5  33761  cdlemc6  33762  cdlemd2  33765  cdleme0e  33783  cdlemeulpq  33786  cdleme01N  33787  cdleme0ex1N  33789  cdleme3g  33800  cdleme3h  33801  cdleme3  33803  cdleme4  33804  cdleme4a  33805  cdleme5  33806  cdleme7aa  33808  cdleme7c  33811  cdleme7d  33812  cdleme7e  33813  cdleme7ga  33814  cdleme7  33815  cdleme9b  33818  cdleme9  33819  cdleme10  33820  cdleme11c  33827  cdleme13  33838  cdleme15b  33841  cdleme15d  33843  cdleme15  33844  cdleme16b  33845  cdleme16e  33848  cdleme16f  33849  cdleme17b  33853  cdleme22gb  33860  cdlemedb  33863  cdlemednpq  33865  cdleme20zN  33867  cdleme20yOLD  33869  cdleme19a  33870  cdleme19c  33872  cdleme20aN  33876  cdleme20c  33878  cdleme20d  33879  cdleme20e  33880  cdleme20j  33885  cdleme20l  33889  cdleme21c  33894  cdleme21ct  33896  cdleme22aa  33906  cdleme22b  33908  cdleme22cN  33909  cdleme22d  33910  cdleme22e  33911  cdleme22eALTN  33912  cdleme22f  33913  cdleme22g  33915  cdleme23a  33916  cdleme23b  33917  cdleme23c  33918  cdleme28a  33937  cdleme35a  34015  cdleme35fnpq  34016  cdleme35b  34017  cdleme35c  34018  cdleme35d  34019  cdleme35e  34020  cdleme35f  34021  cdleme42a  34038  cdleme42c  34039  cdleme42h  34049  cdleme42i  34050  cdlemeg46frv  34092  cdlemeg46vrg  34094  cdlemeg46rgv  34095  cdlemeg46req  34096  cdlemf1  34128  cdlemf2  34129  cdlemg2fv2  34167  cdlemg2m  34171  cdlemg4  34184  cdlemg8b  34195  cdlemg10bALTN  34203  cdlemg10c  34206  cdlemg10  34208  cdlemg12e  34214  cdlemg12f  34215  cdlemg12g  34216  cdlemg12  34217  cdlemg13a  34218  cdlemg17a  34228  cdlemg17dALTN  34231  cdlemg17h  34235  cdlemg17  34244  cdlemg18b  34246  cdlemg19a  34250  cdlemg19  34251  cdlemg27a  34259  cdlemg27b  34263  cdlemg31a  34264  cdlemg31b  34265  cdlemg33b0  34268  cdlemg33a  34273  trlcoabs2N  34289  trlcolem  34293  cdlemg42  34296  cdlemg46  34302  cdlemh1  34382  cdlemk3  34400  cdlemk10  34410  cdlemk12  34417  cdlemkole  34420  cdlemk14  34421  cdlemk15  34422  cdlemk1u  34426  cdlemk5u  34428  cdlemk12u  34439  cdlemk37  34481  cdlemk39  34483  cdlemkid1  34489  cdlemk51  34520  cdlemk52  34521  dia2dimlem1  34632  dia2dimlem2  34633  dia2dimlem3  34634  dia2dimlem10  34641  dia2dimlem12  34643  cdlemm10N  34686  cdlemn2  34763  cdlemn10  34774  dib2dim  34811  dih2dimb  34812  dih2dimbALTN  34813  dihjatcclem1  34986  dihjatcclem2  34987  dihjatcclem4  34989  dvh4dimat  35006