Theorem hlatjcl 37308

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  joincjn 17944  Latclat 18064  Atomscatm 37204  HLchlt 37291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-lub 17979  df-glb 17980  df-join 17981  df-meet 17982  df-lat 18065  df-ats 37208  df-atl 37239  df-cvlat 37263  df-hlat 37292

This theorem is referenced by:  atcvr0eq  37367  2atjm  37386  atbtwn  37387  3dim0  37398  3dimlem3a  37401  3dimlem3OLDN  37403  3dimlem4OLDN  37406  3dim3  37410  2dim  37411  ps-1  37418  hlatexch3N  37421  hlatexch4  37422  ps-2b  37423  3atlem1  37424  3atlem2  37425  llni2  37453  llnle  37459  2at0mat0  37466  2atm  37468  islpln5  37476  lplni2  37478  lplnnle2at  37482  2atnelpln  37485  islpln2a  37489  llncvrlpln2  37498  2atmat  37502  2llnjaN  37507  islvol5  37520  lvoli2  37522  lvolnle3at  37523  3atnelvolN  37527  islvol2aN  37533  4atlem0a  37534  4atlem3  37537  4atlem3a  37538  4atlem3b  37539  4atlem4a  37540  4atlem4b  37541  4atlem4c  37542  4atlem4d  37543  4atlem9  37544  4atlem10a  37545  4atlem10  37547  4atlem11a  37548  4atlem11b  37549  4atlem11  37550  4atlem12a  37551  4atlem12b  37552  4atlem12  37553  4at  37554  4at2  37555  lplncvrlvol2  37556  2lplnja  37560  dalempjqeb  37586  dalemsjteb  37587  dalemtjueb  37588  dalemply  37595  dalem1  37600  dalemcea  37601  dalem3  37605  dalem4  37606  dalem5  37608  dalem-cly  37612  dalem17  37621  dalem21  37635  dalem24  37638  dalem25  37639  dalem27  37640  dalem38  37651  dalem39  37652  dalem43  37656  dalem44  37657  dalem45  37658  dalem55  37668  dalem56  37669  dalem57  37670  2atm2atN  37726  2llnma1b  37727  2llnma3r  37729  llnmod2i2  37804  llnexchb2lem  37809  dalawlem1  37812  dalawlem2  37813  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  dalawlem15  37826  lhp2lt  37942  lhpexle2lem  37950  lhpexle3lem  37952  lhp2at0  37973  lhp2atnle  37974  lhpat3  37987  4atexlempsb  38001  4atexlemqtb  38002  4atexlemunv  38007  4atexlemtlw  38008  4atexlemc  38010  4atexlemnclw  38011  4atexlemcnd  38013  trlval3  38128  trlval4  38129  cdlemc4  38135  cdlemc5  38136  cdlemc6  38137  cdlemd2  38140  cdleme0e  38158  cdlemeulpq  38161  cdleme01N  38162  cdleme0ex1N  38164  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme4  38179  cdleme4a  38180  cdleme5  38181  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme9b  38193  cdleme9  38194  cdleme10  38195  cdleme11c  38202  cdleme13  38213  cdleme15b  38216  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16e  38223  cdleme16f  38224  cdleme17b  38228  cdleme22gb  38235  cdlemedb  38238  cdlemednpq  38240  cdleme20zN  38242  cdleme19a  38244  cdleme19c  38246  cdleme20aN  38250  cdleme20c  38252  cdleme20d  38253  cdleme20e  38254  cdleme20j  38259  cdleme20l  38263  cdleme21c  38268  cdleme21ct  38270  cdleme22aa  38280  cdleme22b  38282  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme22g  38289  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme28a  38311  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme35f  38395  cdleme42a  38412  cdleme42c  38413  cdleme42h  38423  cdleme42i  38424  cdlemeg46frv  38466  cdlemeg46vrg  38468  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemf1  38502  cdlemf2  38503  cdlemg2fv2  38541  cdlemg2m  38545  cdlemg4  38558  cdlemg8b  38569  cdlemg10bALTN  38577  cdlemg10c  38580  cdlemg10  38582  cdlemg12e  38588  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg17a  38602  cdlemg17dALTN  38605  cdlemg17h  38609  cdlemg17  38618  cdlemg18b  38620  cdlemg19a  38624  cdlemg19  38625  cdlemg27a  38633  cdlemg27b  38637  cdlemg31a  38638  cdlemg31b  38639  cdlemg33b0  38642  cdlemg33a  38647  trlcoabs2N  38663  trlcolem  38667  cdlemg42  38670  cdlemg46  38676  cdlemh1  38756  cdlemk3  38774  cdlemk10  38784  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk1u  38800  cdlemk5u  38802  cdlemk12u  38813  cdlemk37  38855  cdlemk39  38857  cdlemkid1  38863  cdlemk51  38894  cdlemk52  38895  dia2dimlem1  39005  dia2dimlem2  39006  dia2dimlem3  39007  dia2dimlem10  39014  dia2dimlem12  39016  cdlemm10N  39059  cdlemn2  39136  cdlemn10  39147  dib2dim  39184  dih2dimb  39185  dih2dimbALTN  39186  dihjatcclem1  39359  dihjatcclem2  39360  dihjatcclem4  39362  dvh4dimat  39379