Theorem hlatjcl 34966

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

Syntax hints:   -> wi 4   /\ w3a 974   = wceq 1383   e. wcel 1804   ` cfv 5578  (class class class)co 6281   Basecbs 14614   joincjn 15552   Latclat 15654   Atomscatm 34863   HLchlt 34950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-lub 15583  df-glb 15584  df-join 15585  df-meet 15586  df-lat 15655  df-ats 34867  df-atl 34898  df-cvlat 34922  df-hlat 34951

This theorem is referenced by:  atcvr0eq  35025  2atjm  35044  atbtwn  35045  3dim0  35056  3dimlem3a  35059  3dimlem3OLDN  35061  3dimlem4OLDN  35064  3dim3  35068  2dim  35069  ps-1  35076  hlatexch3N  35079  hlatexch4  35080  ps-2b  35081  3atlem1  35082  3atlem2  35083  llni2  35111  llnle  35117  2at0mat0  35124  2atm  35126  islpln5  35134  lplni2  35136  lplnnle2at  35140  2atnelpln  35143  islpln2a  35147  llncvrlpln2  35156  2atmat  35160  2llnjaN  35165  islvol5  35178  lvoli2  35180  lvolnle3at  35181  3atnelvolN  35185  islvol2aN  35191  4atlem0a  35192  4atlem3  35195  4atlem3a  35196  4atlem3b  35197  4atlem4a  35198  4atlem4b  35199  4atlem4c  35200  4atlem4d  35201  4atlem9  35202  4atlem10a  35203  4atlem10  35205  4atlem11a  35206  4atlem11b  35207  4atlem11  35208  4atlem12a  35209  4atlem12b  35210  4atlem12  35211  4at  35212  4at2  35213  lplncvrlvol2  35214  2lplnja  35218  dalempjqeb  35244  dalemsjteb  35245  dalemtjueb  35246  dalemply  35253  dalem1  35258  dalemcea  35259  dalem3  35263  dalem4  35264  dalem5  35266  dalem-cly  35270  dalem17  35279  dalem21  35293  dalem24  35296  dalem25  35297  dalem27  35298  dalem38  35309  dalem39  35310  dalem43  35314  dalem44  35315  dalem45  35316  dalem55  35326  dalem56  35327  dalem57  35328  2atm2atN  35384  2llnma1b  35385  2llnma3r  35387  llnmod2i2  35462  llnexchb2lem  35467  dalawlem1  35470  dalawlem2  35471  dalawlem3  35472  dalawlem4  35473  dalawlem5  35474  dalawlem6  35475  dalawlem7  35476  dalawlem8  35477  dalawlem9  35478  dalawlem11  35480  dalawlem12  35481  dalawlem15  35484  lhp2lt  35600  lhpexle2lem  35608  lhpexle3lem  35610  lhp2at0  35631  lhp2atnle  35632  lhpat3  35645  4atexlempsb  35659  4atexlemqtb  35660  4atexlemunv  35665  4atexlemtlw  35666  4atexlemc  35668  4atexlemnclw  35669  4atexlemcnd  35671  trlval3  35787  trlval4  35788  cdlemc4  35794  cdlemc5  35795  cdlemc6  35796  cdlemd2  35799  cdleme0e  35817  cdlemeulpq  35820  cdleme01N  35821  cdleme0ex1N  35823  cdleme3g  35834  cdleme3h  35835  cdleme3  35837  cdleme4  35838  cdleme4a  35839  cdleme5  35840  cdleme7aa  35842  cdleme7c  35845  cdleme7d  35846  cdleme7e  35847  cdleme7ga  35848  cdleme7  35849  cdleme9b  35852  cdleme9  35853  cdleme10  35854  cdleme11c  35861  cdleme13  35872  cdleme15b  35875  cdleme15d  35877  cdleme15  35878  cdleme16b  35879  cdleme16e  35882  cdleme16f  35883  cdleme17b  35887  cdleme22gb  35894  cdlemedb  35897  cdlemednpq  35899  cdleme20zN  35901  cdleme20yOLD  35903  cdleme19a  35904  cdleme19c  35906  cdleme20aN  35910  cdleme20c  35912  cdleme20d  35913  cdleme20e  35914  cdleme20j  35919  cdleme20l  35923  cdleme21c  35928  cdleme21ct  35930  cdleme22aa  35940  cdleme22b  35942  cdleme22cN  35943  cdleme22d  35944  cdleme22e  35945  cdleme22eALTN  35946  cdleme22f  35947  cdleme22g  35949  cdleme23a  35950  cdleme23b  35951  cdleme23c  35952  cdleme28a  35971  cdleme35a  36049  cdleme35fnpq  36050  cdleme35b  36051  cdleme35c  36052  cdleme35d  36053  cdleme35e  36054  cdleme35f  36055  cdleme42a  36072  cdleme42c  36073  cdleme42h  36083  cdleme42i  36084  cdlemeg46frv  36126  cdlemeg46vrg  36128  cdlemeg46rgv  36129  cdlemeg46req  36130  cdlemf1  36162  cdlemf2  36163  cdlemg2fv2  36201  cdlemg2m  36205  cdlemg4  36218  cdlemg8b  36229  cdlemg10bALTN  36237  cdlemg10c  36240  cdlemg10  36242  cdlemg12e  36248  cdlemg12f  36249  cdlemg12g  36250  cdlemg12  36251  cdlemg13a  36252  cdlemg17a  36262  cdlemg17dALTN  36265  cdlemg17h  36269  cdlemg17  36278  cdlemg18b  36280  cdlemg19a  36284  cdlemg19  36285  cdlemg27a  36293  cdlemg27b  36297  cdlemg31a  36298  cdlemg31b  36299  cdlemg33b0  36302  cdlemg33a  36307  trlcoabs2N  36323  trlcolem  36327  cdlemg42  36330  cdlemg46  36336  cdlemh1  36416  cdlemk3  36434  cdlemk10  36444  cdlemk12  36451  cdlemkole  36454  cdlemk14  36455  cdlemk15  36456  cdlemk1u  36460  cdlemk5u  36462  cdlemk12u  36473  cdlemk37  36515  cdlemk39  36517  cdlemkid1  36523  cdlemk51  36554  cdlemk52  36555  dia2dimlem1  36666  dia2dimlem2  36667  dia2dimlem3  36668  dia2dimlem10  36675  dia2dimlem12  36677  cdlemm10N  36720  cdlemn2  36797  cdlemn10  36808  dib2dim  36845  dih2dimb  36846  dih2dimbALTN  36847  dihjatcclem1  37020  dihjatcclem2  37021  dihjatcclem4  37023  dvh4dimat  37040