Theorem hlatjcl 39664

Description: Closure of join operation. Frequently-used special case of latjcl 18366 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 39660	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39586	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 39586	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18366	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	1, 4, 5, 7	syl3an 1161	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  (class class class)co 7360  Basecbs 17140  joincjn 18238  Latclat 18358  Atomscatm 39560  HLchlt 39647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-lub 18271  df-glb 18272  df-join 18273  df-meet 18274  df-lat 18359  df-ats 39564  df-atl 39595  df-cvlat 39619  df-hlat 39648

This theorem is referenced by:  atcvr0eq  39723  2atjm  39742  atbtwn  39743  3dim0  39754  3dimlem3a  39757  3dimlem3OLDN  39759  3dimlem4OLDN  39762  3dim3  39766  2dim  39767  ps-1  39774  hlatexch3N  39777  hlatexch4  39778  ps-2b  39779  3atlem1  39780  3atlem2  39781  llni2  39809  llnle  39815  2at0mat0  39822  2atm  39824  islpln5  39832  lplni2  39834  lplnnle2at  39838  2atnelpln  39841  islpln2a  39845  llncvrlpln2  39854  2atmat  39858  2llnjaN  39863  islvol5  39876  lvoli2  39878  lvolnle3at  39879  3atnelvolN  39883  islvol2aN  39889  4atlem0a  39890  4atlem3  39893  4atlem3a  39894  4atlem3b  39895  4atlem4a  39896  4atlem4b  39897  4atlem4c  39898  4atlem4d  39899  4atlem9  39900  4atlem10a  39901  4atlem10  39903  4atlem11a  39904  4atlem11b  39905  4atlem11  39906  4atlem12a  39907  4atlem12b  39908  4atlem12  39909  4at  39910  4at2  39911  lplncvrlvol2  39912  2lplnja  39916  dalempjqeb  39942  dalemsjteb  39943  dalemtjueb  39944  dalemply  39951  dalem1  39956  dalemcea  39957  dalem3  39961  dalem4  39962  dalem5  39964  dalem-cly  39968  dalem17  39977  dalem21  39991  dalem24  39994  dalem25  39995  dalem27  39996  dalem38  40007  dalem39  40008  dalem43  40012  dalem44  40013  dalem45  40014  dalem55  40024  dalem56  40025  dalem57  40026  2atm2atN  40082  2llnma1b  40083  2llnma3r  40085  llnmod2i2  40160  llnexchb2lem  40165  dalawlem1  40168  dalawlem2  40169  dalawlem3  40170  dalawlem4  40171  dalawlem5  40172  dalawlem6  40173  dalawlem7  40174  dalawlem8  40175  dalawlem9  40176  dalawlem11  40178  dalawlem12  40179  dalawlem15  40182  lhp2lt  40298  lhpexle2lem  40306  lhpexle3lem  40308  lhp2at0  40329  lhp2atnle  40330  lhpat3  40343  4atexlempsb  40357  4atexlemqtb  40358  4atexlemunv  40363  4atexlemtlw  40364  4atexlemc  40366  4atexlemnclw  40367  4atexlemcnd  40369  trlval3  40484  trlval4  40485  cdlemc4  40491  cdlemc5  40492  cdlemc6  40493  cdlemd2  40496  cdleme0e  40514  cdlemeulpq  40517  cdleme01N  40518  cdleme0ex1N  40520  cdleme3g  40531  cdleme3h  40532  cdleme3  40534  cdleme4  40535  cdleme4a  40536  cdleme5  40537  cdleme7aa  40539  cdleme7c  40542  cdleme7d  40543  cdleme7e  40544  cdleme7ga  40545  cdleme7  40546  cdleme9b  40549  cdleme9  40550  cdleme10  40551  cdleme11c  40558  cdleme13  40569  cdleme15b  40572  cdleme15d  40574  cdleme15  40575  cdleme16b  40576  cdleme16e  40579  cdleme16f  40580  cdleme17b  40584  cdleme22gb  40591  cdlemedb  40594  cdlemednpq  40596  cdleme20zN  40598  cdleme19a  40600  cdleme19c  40602  cdleme20aN  40606  cdleme20c  40608  cdleme20d  40609  cdleme20e  40610  cdleme20j  40615  cdleme20l  40619  cdleme21c  40624  cdleme21ct  40626  cdleme22aa  40636  cdleme22b  40638  cdleme22cN  40639  cdleme22d  40640  cdleme22e  40641  cdleme22eALTN  40642  cdleme22f  40643  cdleme22g  40645  cdleme23a  40646  cdleme23b  40647  cdleme23c  40648  cdleme28a  40667  cdleme35a  40745  cdleme35fnpq  40746  cdleme35b  40747  cdleme35c  40748  cdleme35d  40749  cdleme35e  40750  cdleme35f  40751  cdleme42a  40768  cdleme42c  40769  cdleme42h  40779  cdleme42i  40780  cdlemeg46frv  40822  cdlemeg46vrg  40824  cdlemeg46rgv  40825  cdlemeg46req  40826  cdlemf1  40858  cdlemf2  40859  cdlemg2fv2  40897  cdlemg2m  40901  cdlemg4  40914  cdlemg8b  40925  cdlemg10bALTN  40933  cdlemg10c  40936  cdlemg10  40938  cdlemg12e  40944  cdlemg12f  40945  cdlemg12g  40946  cdlemg12  40947  cdlemg13a  40948  cdlemg17a  40958  cdlemg17dALTN  40961  cdlemg17h  40965  cdlemg17  40974  cdlemg18b  40976  cdlemg19a  40980  cdlemg19  40981  cdlemg27a  40989  cdlemg27b  40993  cdlemg31a  40994  cdlemg31b  40995  cdlemg33b0  40998  cdlemg33a  41003  trlcoabs2N  41019  trlcolem  41023  cdlemg42  41026  cdlemg46  41032  cdlemh1  41112  cdlemk3  41130  cdlemk10  41140  cdlemk12  41147  cdlemkole  41150  cdlemk14  41151  cdlemk15  41152  cdlemk1u  41156  cdlemk5u  41158  cdlemk12u  41169  cdlemk37  41211  cdlemk39  41213  cdlemkid1  41219  cdlemk51  41250  cdlemk52  41251  dia2dimlem1  41361  dia2dimlem2  41362  dia2dimlem3  41363  dia2dimlem10  41370  dia2dimlem12  41372  cdlemm10N  41415  cdlemn2  41492  cdlemn10  41503  dib2dim  41540  dih2dimb  41541  dih2dimbALTN  41542  dihjatcclem1  41715  dihjatcclem2  41716  dihjatcclem4  41718  dvh4dimat  41735