Theorem hlatjcl 37902

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ‘cfv 6501  (class class class)co 7362  Basecbs 17094  joincjn 18214  Latclat 18334  Atomscatm 37798  HLchlt 37885

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-lub 18249  df-glb 18250  df-join 18251  df-meet 18252  df-lat 18335  df-ats 37802  df-atl 37833  df-cvlat 37857  df-hlat 37886

This theorem is referenced by:  atcvr0eq  37962  2atjm  37981  atbtwn  37982  3dim0  37993  3dimlem3a  37996  3dimlem3OLDN  37998  3dimlem4OLDN  38001  3dim3  38005  2dim  38006  ps-1  38013  hlatexch3N  38016  hlatexch4  38017  ps-2b  38018  3atlem1  38019  3atlem2  38020  llni2  38048  llnle  38054  2at0mat0  38061  2atm  38063  islpln5  38071  lplni2  38073  lplnnle2at  38077  2atnelpln  38080  islpln2a  38084  llncvrlpln2  38093  2atmat  38097  2llnjaN  38102  islvol5  38115  lvoli2  38117  lvolnle3at  38118  3atnelvolN  38122  islvol2aN  38128  4atlem0a  38129  4atlem3  38132  4atlem3a  38133  4atlem3b  38134  4atlem4a  38135  4atlem4b  38136  4atlem4c  38137  4atlem4d  38138  4atlem9  38139  4atlem10a  38140  4atlem10  38142  4atlem11a  38143  4atlem11b  38144  4atlem11  38145  4atlem12a  38146  4atlem12b  38147  4atlem12  38148  4at  38149  4at2  38150  lplncvrlvol2  38151  2lplnja  38155  dalempjqeb  38181  dalemsjteb  38182  dalemtjueb  38183  dalemply  38190  dalem1  38195  dalemcea  38196  dalem3  38200  dalem4  38201  dalem5  38203  dalem-cly  38207  dalem17  38216  dalem21  38230  dalem24  38233  dalem25  38234  dalem27  38235  dalem38  38246  dalem39  38247  dalem43  38251  dalem44  38252  dalem45  38253  dalem55  38263  dalem56  38264  dalem57  38265  2atm2atN  38321  2llnma1b  38322  2llnma3r  38324  llnmod2i2  38399  llnexchb2lem  38404  dalawlem1  38407  dalawlem2  38408  dalawlem3  38409  dalawlem4  38410  dalawlem5  38411  dalawlem6  38412  dalawlem7  38413  dalawlem8  38414  dalawlem9  38415  dalawlem11  38417  dalawlem12  38418  dalawlem15  38421  lhp2lt  38537  lhpexle2lem  38545  lhpexle3lem  38547  lhp2at0  38568  lhp2atnle  38569  lhpat3  38582  4atexlempsb  38596  4atexlemqtb  38597  4atexlemunv  38602  4atexlemtlw  38603  4atexlemc  38605  4atexlemnclw  38606  4atexlemcnd  38608  trlval3  38723  trlval4  38724  cdlemc4  38730  cdlemc5  38731  cdlemc6  38732  cdlemd2  38735  cdleme0e  38753  cdlemeulpq  38756  cdleme01N  38757  cdleme0ex1N  38759  cdleme3g  38770  cdleme3h  38771  cdleme3  38773  cdleme4  38774  cdleme4a  38775  cdleme5  38776  cdleme7aa  38778  cdleme7c  38781  cdleme7d  38782  cdleme7e  38783  cdleme7ga  38784  cdleme7  38785  cdleme9b  38788  cdleme9  38789  cdleme10  38790  cdleme11c  38797  cdleme13  38808  cdleme15b  38811  cdleme15d  38813  cdleme15  38814  cdleme16b  38815  cdleme16e  38818  cdleme16f  38819  cdleme17b  38823  cdleme22gb  38830  cdlemedb  38833  cdlemednpq  38835  cdleme20zN  38837  cdleme19a  38839  cdleme19c  38841  cdleme20aN  38845  cdleme20c  38847  cdleme20d  38848  cdleme20e  38849  cdleme20j  38854  cdleme20l  38858  cdleme21c  38863  cdleme21ct  38865  cdleme22aa  38875  cdleme22b  38877  cdleme22cN  38878  cdleme22d  38879  cdleme22e  38880  cdleme22eALTN  38881  cdleme22f  38882  cdleme22g  38884  cdleme23a  38885  cdleme23b  38886  cdleme23c  38887  cdleme28a  38906  cdleme35a  38984  cdleme35fnpq  38985  cdleme35b  38986  cdleme35c  38987  cdleme35d  38988  cdleme35e  38989  cdleme35f  38990  cdleme42a  39007  cdleme42c  39008  cdleme42h  39018  cdleme42i  39019  cdlemeg46frv  39061  cdlemeg46vrg  39063  cdlemeg46rgv  39064  cdlemeg46req  39065  cdlemf1  39097  cdlemf2  39098  cdlemg2fv2  39136  cdlemg2m  39140  cdlemg4  39153  cdlemg8b  39164  cdlemg10bALTN  39172  cdlemg10c  39175  cdlemg10  39177  cdlemg12e  39183  cdlemg12f  39184  cdlemg12g  39185  cdlemg12  39186  cdlemg13a  39187  cdlemg17a  39197  cdlemg17dALTN  39200  cdlemg17h  39204  cdlemg17  39213  cdlemg18b  39215  cdlemg19a  39219  cdlemg19  39220  cdlemg27a  39228  cdlemg27b  39232  cdlemg31a  39233  cdlemg31b  39234  cdlemg33b0  39237  cdlemg33a  39242  trlcoabs2N  39258  trlcolem  39262  cdlemg42  39265  cdlemg46  39271  cdlemh1  39351  cdlemk3  39369  cdlemk10  39379  cdlemk12  39386  cdlemkole  39389  cdlemk14  39390  cdlemk15  39391  cdlemk1u  39395  cdlemk5u  39397  cdlemk12u  39408  cdlemk37  39450  cdlemk39  39452  cdlemkid1  39458  cdlemk51  39489  cdlemk52  39490  dia2dimlem1  39600  dia2dimlem2  39601  dia2dimlem3  39602  dia2dimlem10  39609  dia2dimlem12  39611  cdlemm10N  39654  cdlemn2  39731  cdlemn10  39742  dib2dim  39779  dih2dimb  39780  dih2dimbALTN  39781  dihjatcclem1  39954  dihjatcclem2  39955  dihjatcclem4  39957  dvh4dimat  39974