Theorem hlatjcl 34653

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

Syntax hints:   -> wi 4   /\ w3a 1037   = wceq 1483   e. wcel 1990   ` cfv 5888  (class class class)co 6650   Basecbs 15857   joincjn 16944   Latclat 17045   Atomscatm 34550   HLchlt 34637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-lub 16974  df-glb 16975  df-join 16976  df-meet 16977  df-lat 17046  df-ats 34554  df-atl 34585  df-cvlat 34609  df-hlat 34638

This theorem is referenced by:  atcvr0eq  34712  2atjm  34731  atbtwn  34732  3dim0  34743  3dimlem3a  34746  3dimlem3OLDN  34748  3dimlem4OLDN  34751  3dim3  34755  2dim  34756  ps-1  34763  hlatexch3N  34766  hlatexch4  34767  ps-2b  34768  3atlem1  34769  3atlem2  34770  llni2  34798  llnle  34804  2at0mat0  34811  2atm  34813  islpln5  34821  lplni2  34823  lplnnle2at  34827  2atnelpln  34830  islpln2a  34834  llncvrlpln2  34843  2atmat  34847  2llnjaN  34852  islvol5  34865  lvoli2  34867  lvolnle3at  34868  3atnelvolN  34872  islvol2aN  34878  4atlem0a  34879  4atlem3  34882  4atlem3a  34883  4atlem3b  34884  4atlem4a  34885  4atlem4b  34886  4atlem4c  34887  4atlem4d  34888  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem11b  34894  4atlem11  34895  4atlem12a  34896  4atlem12b  34897  4atlem12  34898  4at  34899  4at2  34900  lplncvrlvol2  34901  2lplnja  34905  dalempjqeb  34931  dalemsjteb  34932  dalemtjueb  34933  dalemply  34940  dalem1  34945  dalemcea  34946  dalem3  34950  dalem4  34951  dalem5  34953  dalem-cly  34957  dalem17  34966  dalem21  34980  dalem24  34983  dalem25  34984  dalem27  34985  dalem38  34996  dalem39  34997  dalem43  35001  dalem44  35002  dalem45  35003  dalem55  35013  dalem56  35014  dalem57  35015  2atm2atN  35071  2llnma1b  35072  2llnma3r  35074  llnmod2i2  35149  llnexchb2lem  35154  dalawlem1  35157  dalawlem2  35158  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem15  35171  lhp2lt  35287  lhpexle2lem  35295  lhpexle3lem  35297  lhp2at0  35318  lhp2atnle  35319  lhpat3  35332  4atexlempsb  35346  4atexlemqtb  35347  4atexlemunv  35352  4atexlemtlw  35353  4atexlemc  35355  4atexlemnclw  35356  4atexlemcnd  35358  trlval3  35474  trlval4  35475  cdlemc4  35481  cdlemc5  35482  cdlemc6  35483  cdlemd2  35486  cdleme0e  35504  cdlemeulpq  35507  cdleme01N  35508  cdleme0ex1N  35510  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4  35525  cdleme4a  35526  cdleme5  35527  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme9b  35539  cdleme9  35540  cdleme10  35541  cdleme11c  35548  cdleme13  35559  cdleme15b  35562  cdleme15d  35564  cdleme15  35565  cdleme16b  35566  cdleme16e  35569  cdleme16f  35570  cdleme17b  35574  cdleme22gb  35581  cdlemedb  35584  cdlemednpq  35586  cdleme20zN  35588  cdleme20yOLD  35590  cdleme19a  35591  cdleme19c  35593  cdleme20aN  35597  cdleme20c  35599  cdleme20d  35600  cdleme20e  35601  cdleme20j  35606  cdleme20l  35610  cdleme21c  35615  cdleme21ct  35617  cdleme22aa  35627  cdleme22b  35629  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme22g  35636  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme28a  35658  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme35f  35742  cdleme42a  35759  cdleme42c  35760  cdleme42h  35770  cdleme42i  35771  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemf1  35849  cdlemf2  35850  cdlemg2fv2  35888  cdlemg2m  35892  cdlemg4  35905  cdlemg8b  35916  cdlemg10bALTN  35924  cdlemg10c  35927  cdlemg10  35929  cdlemg12e  35935  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg17a  35949  cdlemg17dALTN  35952  cdlemg17h  35956  cdlemg17  35965  cdlemg18b  35967  cdlemg19a  35971  cdlemg19  35972  cdlemg27a  35980  cdlemg27b  35984  cdlemg31a  35985  cdlemg31b  35986  cdlemg33b0  35989  cdlemg33a  35994  trlcoabs2N  36010  trlcolem  36014  cdlemg42  36017  cdlemg46  36023  cdlemh1  36103  cdlemk3  36121  cdlemk10  36131  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk1u  36147  cdlemk5u  36149  cdlemk12u  36160  cdlemk37  36202  cdlemk39  36204  cdlemkid1  36210  cdlemk51  36241  cdlemk52  36242  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  dia2dimlem10  36362  dia2dimlem12  36364  cdlemm10N  36407  cdlemn2  36484  cdlemn10  36495  dib2dim  36532  dih2dimb  36533  dih2dimbALTN  36534  dihjatcclem1  36707  dihjatcclem2  36708  dihjatcclem4  36710  dvh4dimat  36727