Theorem hlatjcl 39991

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

Hypotheses

Ref	Expression
hlatjcl.b	⊢ 𝐵 = (Base‘𝐾)
hlatjcl.j	⊢ ∨ = (join‘𝐾)
hlatjcl.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
hlatjcl	⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Proof of Theorem hlatjcl

Step	Hyp	Ref	Expression
1		hllat 39987	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39913	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 39913	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18471	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	1, 4, 5, 7	syl3an 1173	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  joincjn 18343  Latclat 18463  Atomscatm 39887  HLchlt 39974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-lub 18376  df-glb 18377  df-join 18378  df-meet 18379  df-lat 18464  df-ats 39891  df-atl 39922  df-cvlat 39946  df-hlat 39975

This theorem is referenced by:  atcvr0eq  40050  2atjm  40069  atbtwn  40070  3dim0  40081  3dimlem3a  40084  3dimlem3OLDN  40086  3dimlem4OLDN  40089  3dim3  40093  2dim  40094  ps-1  40101  hlatexch3N  40104  hlatexch4  40105  ps-2b  40106  3atlem1  40107  3atlem2  40108  llni2  40136  llnle  40142  2at0mat0  40149  2atm  40151  islpln5  40159  lplni2  40161  lplnnle2at  40165  2atnelpln  40168  islpln2a  40172  llncvrlpln2  40181  2atmat  40185  2llnjaN  40190  islvol5  40203  lvoli2  40205  lvolnle3at  40206  3atnelvolN  40210  islvol2aN  40216  4atlem0a  40217  4atlem3  40220  4atlem3a  40221  4atlem3b  40222  4atlem4a  40223  4atlem4b  40224  4atlem4c  40225  4atlem4d  40226  4atlem9  40227  4atlem10a  40228  4atlem10  40230  4atlem11a  40231  4atlem11b  40232  4atlem11  40233  4atlem12a  40234  4atlem12b  40235  4atlem12  40236  4at  40237  4at2  40238  lplncvrlvol2  40239  2lplnja  40243  dalempjqeb  40269  dalemsjteb  40270  dalemtjueb  40271  dalemply  40278  dalem1  40283  dalemcea  40284  dalem3  40288  dalem4  40289  dalem5  40291  dalem-cly  40295  dalem17  40304  dalem21  40318  dalem24  40321  dalem25  40322  dalem27  40323  dalem38  40334  dalem39  40335  dalem43  40339  dalem44  40340  dalem45  40341  dalem55  40351  dalem56  40352  dalem57  40353  2atm2atN  40409  2llnma1b  40410  2llnma3r  40412  llnmod2i2  40487  llnexchb2lem  40492  dalawlem1  40495  dalawlem2  40496  dalawlem3  40497  dalawlem4  40498  dalawlem5  40499  dalawlem6  40500  dalawlem7  40501  dalawlem8  40502  dalawlem9  40503  dalawlem11  40505  dalawlem12  40506  dalawlem15  40509  lhp2lt  40625  lhpexle2lem  40633  lhpexle3lem  40635  lhp2at0  40656  lhp2atnle  40657  lhpat3  40670  4atexlempsb  40684  4atexlemqtb  40685  4atexlemunv  40690  4atexlemtlw  40691  4atexlemc  40693  4atexlemnclw  40694  4atexlemcnd  40696  trlval3  40811  trlval4  40812  cdlemc4  40818  cdlemc5  40819  cdlemc6  40820  cdlemd2  40823  cdleme0e  40841  cdlemeulpq  40844  cdleme01N  40845  cdleme0ex1N  40847  cdleme3g  40858  cdleme3h  40859  cdleme3  40861  cdleme4  40862  cdleme4a  40863  cdleme5  40864  cdleme7aa  40866  cdleme7c  40869  cdleme7d  40870  cdleme7e  40871  cdleme7ga  40872  cdleme7  40873  cdleme9b  40876  cdleme9  40877  cdleme10  40878  cdleme11c  40885  cdleme13  40896  cdleme15b  40899  cdleme15d  40901  cdleme15  40902  cdleme16b  40903  cdleme16e  40906  cdleme16f  40907  cdleme17b  40911  cdleme22gb  40918  cdlemedb  40921  cdlemednpq  40923  cdleme20zN  40925  cdleme19a  40927  cdleme19c  40929  cdleme20aN  40933  cdleme20c  40935  cdleme20d  40936  cdleme20e  40937  cdleme20j  40942  cdleme20l  40946  cdleme21c  40951  cdleme21ct  40953  cdleme22aa  40963  cdleme22b  40965  cdleme22cN  40966  cdleme22d  40967  cdleme22e  40968  cdleme22eALTN  40969  cdleme22f  40970  cdleme22g  40972  cdleme23a  40973  cdleme23b  40974  cdleme23c  40975  cdleme28a  40994  cdleme35a  41072  cdleme35fnpq  41073  cdleme35b  41074  cdleme35c  41075  cdleme35d  41076  cdleme35e  41077  cdleme35f  41078  cdleme42a  41095  cdleme42c  41096  cdleme42h  41106  cdleme42i  41107  cdlemeg46frv  41149  cdlemeg46vrg  41151  cdlemeg46rgv  41152  cdlemeg46req  41153  cdlemf1  41185  cdlemf2  41186  cdlemg2fv2  41224  cdlemg2m  41228  cdlemg4  41241  cdlemg8b  41252  cdlemg10bALTN  41260  cdlemg10c  41263  cdlemg10  41265  cdlemg12e  41271  cdlemg12f  41272  cdlemg12g  41273  cdlemg12  41274  cdlemg13a  41275  cdlemg17a  41285  cdlemg17dALTN  41288  cdlemg17h  41292  cdlemg17  41301  cdlemg18b  41303  cdlemg19a  41307  cdlemg19  41308  cdlemg27a  41316  cdlemg27b  41320  cdlemg31a  41321  cdlemg31b  41322  cdlemg33b0  41325  cdlemg33a  41330  trlcoabs2N  41346  trlcolem  41350  cdlemg42  41353  cdlemg46  41359  cdlemh1  41439  cdlemk3  41457  cdlemk10  41467  cdlemk12  41474  cdlemkole  41477  cdlemk14  41478  cdlemk15  41479  cdlemk1u  41483  cdlemk5u  41485  cdlemk12u  41496  cdlemk37  41538  cdlemk39  41540  cdlemkid1  41546  cdlemk51  41577  cdlemk52  41578  dia2dimlem1  41688  dia2dimlem2  41689  dia2dimlem3  41690  dia2dimlem10  41697  dia2dimlem12  41699  cdlemm10N  41742  cdlemn2  41819  cdlemn10  41830  dib2dim  41867  dih2dimb  41868  dih2dimbALTN  41869  dihjatcclem1  42042  dihjatcclem2  42043  dihjatcclem4  42045  dvh4dimat  42062