Theorem hlatjcl 40161

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  Basecbs 17264  joincjn 18362  Latclat 18482  Atomscatm 40057  HLchlt 40144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-lub 18395  df-glb 18396  df-join 18397  df-meet 18398  df-lat 18483  df-ats 40061  df-atl 40092  df-cvlat 40116  df-hlat 40145

This theorem is referenced by:  atcvr0eq  40220  2atjm  40239  atbtwn  40240  3dim0  40251  3dimlem3a  40254  3dimlem3OLDN  40256  3dimlem4OLDN  40259  3dim3  40263  2dim  40264  ps-1  40271  hlatexch3N  40274  hlatexch4  40275  ps-2b  40276  3atlem1  40277  3atlem2  40278  llni2  40306  llnle  40312  2at0mat0  40319  2atm  40321  islpln5  40329  lplni2  40331  lplnnle2at  40335  2atnelpln  40338  islpln2a  40342  llncvrlpln2  40351  2atmat  40355  2llnjaN  40360  islvol5  40373  lvoli2  40375  lvolnle3at  40376  3atnelvolN  40380  islvol2aN  40386  4atlem0a  40387  4atlem3  40390  4atlem3a  40391  4atlem3b  40392  4atlem4a  40393  4atlem4b  40394  4atlem4c  40395  4atlem4d  40396  4atlem9  40397  4atlem10a  40398  4atlem10  40400  4atlem11a  40401  4atlem11b  40402  4atlem11  40403  4atlem12a  40404  4atlem12b  40405  4atlem12  40406  4at  40407  4at2  40408  lplncvrlvol2  40409  2lplnja  40413  dalempjqeb  40439  dalemsjteb  40440  dalemtjueb  40441  dalemply  40448  dalem1  40453  dalemcea  40454  dalem3  40458  dalem4  40459  dalem5  40461  dalem-cly  40465  dalem17  40474  dalem21  40488  dalem24  40491  dalem25  40492  dalem27  40493  dalem38  40504  dalem39  40505  dalem43  40509  dalem44  40510  dalem45  40511  dalem55  40521  dalem56  40522  dalem57  40523  2atm2atN  40579  2llnma1b  40580  2llnma3r  40582  llnmod2i2  40657  llnexchb2lem  40662  dalawlem1  40665  dalawlem2  40666  dalawlem3  40667  dalawlem4  40668  dalawlem5  40669  dalawlem6  40670  dalawlem7  40671  dalawlem8  40672  dalawlem9  40673  dalawlem11  40675  dalawlem12  40676  dalawlem15  40679  lhp2lt  40795  lhpexle2lem  40803  lhpexle3lem  40805  lhp2at0  40826  lhp2atnle  40827  lhpat3  40840  4atexlempsb  40854  4atexlemqtb  40855  4atexlemunv  40860  4atexlemtlw  40861  4atexlemc  40863  4atexlemnclw  40864  4atexlemcnd  40866  trlval3  40981  trlval4  40982  cdlemc4  40988  cdlemc5  40989  cdlemc6  40990  cdlemd2  40993  cdleme0e  41011  cdlemeulpq  41014  cdleme01N  41015  cdleme0ex1N  41017  cdleme3g  41028  cdleme3h  41029  cdleme3  41031  cdleme4  41032  cdleme4a  41033  cdleme5  41034  cdleme7aa  41036  cdleme7c  41039  cdleme7d  41040  cdleme7e  41041  cdleme7ga  41042  cdleme7  41043  cdleme9b  41046  cdleme9  41047  cdleme10  41048  cdleme11c  41055  cdleme13  41066  cdleme15b  41069  cdleme15d  41071  cdleme15  41072  cdleme16b  41073  cdleme16e  41076  cdleme16f  41077  cdleme17b  41081  cdleme22gb  41088  cdlemedb  41091  cdlemednpq  41093  cdleme20zN  41095  cdleme19a  41097  cdleme19c  41099  cdleme20aN  41103  cdleme20c  41105  cdleme20d  41106  cdleme20e  41107  cdleme20j  41112  cdleme20l  41116  cdleme21c  41121  cdleme21ct  41123  cdleme22aa  41133  cdleme22b  41135  cdleme22cN  41136  cdleme22d  41137  cdleme22e  41138  cdleme22eALTN  41139  cdleme22f  41140  cdleme22g  41142  cdleme23a  41143  cdleme23b  41144  cdleme23c  41145  cdleme28a  41164  cdleme35a  41242  cdleme35fnpq  41243  cdleme35b  41244  cdleme35c  41245  cdleme35d  41246  cdleme35e  41247  cdleme35f  41248  cdleme42a  41265  cdleme42c  41266  cdleme42h  41276  cdleme42i  41277  cdlemeg46frv  41319  cdlemeg46vrg  41321  cdlemeg46rgv  41322  cdlemeg46req  41323  cdlemf1  41355  cdlemf2  41356  cdlemg2fv2  41394  cdlemg2m  41398  cdlemg4  41411  cdlemg8b  41422  cdlemg10bALTN  41430  cdlemg10c  41433  cdlemg10  41435  cdlemg12e  41441  cdlemg12f  41442  cdlemg12g  41443  cdlemg12  41444  cdlemg13a  41445  cdlemg17a  41455  cdlemg17dALTN  41458  cdlemg17h  41462  cdlemg17  41471  cdlemg18b  41473  cdlemg19a  41477  cdlemg19  41478  cdlemg27a  41486  cdlemg27b  41490  cdlemg31a  41491  cdlemg31b  41492  cdlemg33b0  41495  cdlemg33a  41500  trlcoabs2N  41516  trlcolem  41520  cdlemg42  41523  cdlemg46  41529  cdlemh1  41609  cdlemk3  41627  cdlemk10  41637  cdlemk12  41644  cdlemkole  41647  cdlemk14  41648  cdlemk15  41649  cdlemk1u  41653  cdlemk5u  41655  cdlemk12u  41666  cdlemk37  41708  cdlemk39  41710  cdlemkid1  41716  cdlemk51  41747  cdlemk52  41748  dia2dimlem1  41858  dia2dimlem2  41859  dia2dimlem3  41860  dia2dimlem10  41867  dia2dimlem12  41869  cdlemm10N  41912  cdlemn2  41989  cdlemn10  42000  dib2dim  42037  dih2dimb  42038  dih2dimbALTN  42039  dihjatcclem1  42212  dihjatcclem2  42213  dihjatcclem4  42215  dvh4dimat  42232