Theorem hlatjcl 35507

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

Syntax hints:   -> wi 4   /\ w3a 971   = wceq 1398   e. wcel 1823   ` cfv 5570  (class class class)co 6270   Basecbs 14719   joincjn 15775   Latclat 15877   Atomscatm 35404   HLchlt 35491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-lub 15806  df-glb 15807  df-join 15808  df-meet 15809  df-lat 15878  df-ats 35408  df-atl 35439  df-cvlat 35463  df-hlat 35492

This theorem is referenced by:  atcvr0eq  35566  2atjm  35585  atbtwn  35586  3dim0  35597  3dimlem3a  35600  3dimlem3OLDN  35602  3dimlem4OLDN  35605  3dim3  35609  2dim  35610  ps-1  35617  hlatexch3N  35620  hlatexch4  35621  ps-2b  35622  3atlem1  35623  3atlem2  35624  llni2  35652  llnle  35658  2at0mat0  35665  2atm  35667  islpln5  35675  lplni2  35677  lplnnle2at  35681  2atnelpln  35684  islpln2a  35688  llncvrlpln2  35697  2atmat  35701  2llnjaN  35706  islvol5  35719  lvoli2  35721  lvolnle3at  35722  3atnelvolN  35726  islvol2aN  35732  4atlem0a  35733  4atlem3  35736  4atlem3a  35737  4atlem3b  35738  4atlem4a  35739  4atlem4b  35740  4atlem4c  35741  4atlem4d  35742  4atlem9  35743  4atlem10a  35744  4atlem10  35746  4atlem11a  35747  4atlem11b  35748  4atlem11  35749  4atlem12a  35750  4atlem12b  35751  4atlem12  35752  4at  35753  4at2  35754  lplncvrlvol2  35755  2lplnja  35759  dalempjqeb  35785  dalemsjteb  35786  dalemtjueb  35787  dalemply  35794  dalem1  35799  dalemcea  35800  dalem3  35804  dalem4  35805  dalem5  35807  dalem-cly  35811  dalem17  35820  dalem21  35834  dalem24  35837  dalem25  35838  dalem27  35839  dalem38  35850  dalem39  35851  dalem43  35855  dalem44  35856  dalem45  35857  dalem55  35867  dalem56  35868  dalem57  35869  2atm2atN  35925  2llnma1b  35926  2llnma3r  35928  llnmod2i2  36003  llnexchb2lem  36008  dalawlem1  36011  dalawlem2  36012  dalawlem3  36013  dalawlem4  36014  dalawlem5  36015  dalawlem6  36016  dalawlem7  36017  dalawlem8  36018  dalawlem9  36019  dalawlem11  36021  dalawlem12  36022  dalawlem15  36025  lhp2lt  36141  lhpexle2lem  36149  lhpexle3lem  36151  lhp2at0  36172  lhp2atnle  36173  lhpat3  36186  4atexlempsb  36200  4atexlemqtb  36201  4atexlemunv  36206  4atexlemtlw  36207  4atexlemc  36209  4atexlemnclw  36210  4atexlemcnd  36212  trlval3  36328  trlval4  36329  cdlemc4  36335  cdlemc5  36336  cdlemc6  36337  cdlemd2  36340  cdleme0e  36358  cdlemeulpq  36361  cdleme01N  36362  cdleme0ex1N  36364  cdleme3g  36375  cdleme3h  36376  cdleme3  36378  cdleme4  36379  cdleme4a  36380  cdleme5  36381  cdleme7aa  36383  cdleme7c  36386  cdleme7d  36387  cdleme7e  36388  cdleme7ga  36389  cdleme7  36390  cdleme9b  36393  cdleme9  36394  cdleme10  36395  cdleme11c  36402  cdleme13  36413  cdleme15b  36416  cdleme15d  36418  cdleme15  36419  cdleme16b  36420  cdleme16e  36423  cdleme16f  36424  cdleme17b  36428  cdleme22gb  36435  cdlemedb  36438  cdlemednpq  36440  cdleme20zN  36442  cdleme20yOLD  36444  cdleme19a  36445  cdleme19c  36447  cdleme20aN  36451  cdleme20c  36453  cdleme20d  36454  cdleme20e  36455  cdleme20j  36460  cdleme20l  36464  cdleme21c  36469  cdleme21ct  36471  cdleme22aa  36481  cdleme22b  36483  cdleme22cN  36484  cdleme22d  36485  cdleme22e  36486  cdleme22eALTN  36487  cdleme22f  36488  cdleme22g  36490  cdleme23a  36491  cdleme23b  36492  cdleme23c  36493  cdleme28a  36512  cdleme35a  36590  cdleme35fnpq  36591  cdleme35b  36592  cdleme35c  36593  cdleme35d  36594  cdleme35e  36595  cdleme35f  36596  cdleme42a  36613  cdleme42c  36614  cdleme42h  36624  cdleme42i  36625  cdlemeg46frv  36667  cdlemeg46vrg  36669  cdlemeg46rgv  36670  cdlemeg46req  36671  cdlemf1  36703  cdlemf2  36704  cdlemg2fv2  36742  cdlemg2m  36746  cdlemg4  36759  cdlemg8b  36770  cdlemg10bALTN  36778  cdlemg10c  36781  cdlemg10  36783  cdlemg12e  36789  cdlemg12f  36790  cdlemg12g  36791  cdlemg12  36792  cdlemg13a  36793  cdlemg17a  36803  cdlemg17dALTN  36806  cdlemg17h  36810  cdlemg17  36819  cdlemg18b  36821  cdlemg19a  36825  cdlemg19  36826  cdlemg27a  36834  cdlemg27b  36838  cdlemg31a  36839  cdlemg31b  36840  cdlemg33b0  36843  cdlemg33a  36848  trlcoabs2N  36864  trlcolem  36868  cdlemg42  36871  cdlemg46  36877  cdlemh1  36957  cdlemk3  36975  cdlemk10  36985  cdlemk12  36992  cdlemkole  36995  cdlemk14  36996  cdlemk15  36997  cdlemk1u  37001  cdlemk5u  37003  cdlemk12u  37014  cdlemk37  37056  cdlemk39  37058  cdlemkid1  37064  cdlemk51  37095  cdlemk52  37096  dia2dimlem1  37207  dia2dimlem2  37208  dia2dimlem3  37209  dia2dimlem10  37216  dia2dimlem12  37218  cdlemm10N  37261  cdlemn2  37338  cdlemn10  37349  dib2dim  37386  dih2dimb  37387  dih2dimbALTN  37388  dihjatcclem1  37561  dihjatcclem2  37562  dihjatcclem4  37564  dvh4dimat  37581