Theorem hlatjcl 39830

Description: Closure of join operation. Frequently-used special case of latjcl 18399 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 39826	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39752	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 39752	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18399	. 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 7361  Basecbs 17173  joincjn 18271  Latclat 18391  Atomscatm 39726  HLchlt 39813

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 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

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 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  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 7318  df-ov 7364  df-oprab 7365  df-lub 18304  df-glb 18305  df-join 18306  df-meet 18307  df-lat 18392  df-ats 39730  df-atl 39761  df-cvlat 39785  df-hlat 39814

This theorem is referenced by:  atcvr0eq  39889  2atjm  39908  atbtwn  39909  3dim0  39920  3dimlem3a  39923  3dimlem3OLDN  39925  3dimlem4OLDN  39928  3dim3  39932  2dim  39933  ps-1  39940  hlatexch3N  39943  hlatexch4  39944  ps-2b  39945  3atlem1  39946  3atlem2  39947  llni2  39975  llnle  39981  2at0mat0  39988  2atm  39990  islpln5  39998  lplni2  40000  lplnnle2at  40004  2atnelpln  40007  islpln2a  40011  llncvrlpln2  40020  2atmat  40024  2llnjaN  40029  islvol5  40042  lvoli2  40044  lvolnle3at  40045  3atnelvolN  40049  islvol2aN  40055  4atlem0a  40056  4atlem3  40059  4atlem3a  40060  4atlem3b  40061  4atlem4a  40062  4atlem4b  40063  4atlem4c  40064  4atlem4d  40065  4atlem9  40066  4atlem10a  40067  4atlem10  40069  4atlem11a  40070  4atlem11b  40071  4atlem11  40072  4atlem12a  40073  4atlem12b  40074  4atlem12  40075  4at  40076  4at2  40077  lplncvrlvol2  40078  2lplnja  40082  dalempjqeb  40108  dalemsjteb  40109  dalemtjueb  40110  dalemply  40117  dalem1  40122  dalemcea  40123  dalem3  40127  dalem4  40128  dalem5  40130  dalem-cly  40134  dalem17  40143  dalem21  40157  dalem24  40160  dalem25  40161  dalem27  40162  dalem38  40173  dalem39  40174  dalem43  40178  dalem44  40179  dalem45  40180  dalem55  40190  dalem56  40191  dalem57  40192  2atm2atN  40248  2llnma1b  40249  2llnma3r  40251  llnmod2i2  40326  llnexchb2lem  40331  dalawlem1  40334  dalawlem2  40335  dalawlem3  40336  dalawlem4  40337  dalawlem5  40338  dalawlem6  40339  dalawlem7  40340  dalawlem8  40341  dalawlem9  40342  dalawlem11  40344  dalawlem12  40345  dalawlem15  40348  lhp2lt  40464  lhpexle2lem  40472  lhpexle3lem  40474  lhp2at0  40495  lhp2atnle  40496  lhpat3  40509  4atexlempsb  40523  4atexlemqtb  40524  4atexlemunv  40529  4atexlemtlw  40530  4atexlemc  40532  4atexlemnclw  40533  4atexlemcnd  40535  trlval3  40650  trlval4  40651  cdlemc4  40657  cdlemc5  40658  cdlemc6  40659  cdlemd2  40662  cdleme0e  40680  cdlemeulpq  40683  cdleme01N  40684  cdleme0ex1N  40686  cdleme3g  40697  cdleme3h  40698  cdleme3  40700  cdleme4  40701  cdleme4a  40702  cdleme5  40703  cdleme7aa  40705  cdleme7c  40708  cdleme7d  40709  cdleme7e  40710  cdleme7ga  40711  cdleme7  40712  cdleme9b  40715  cdleme9  40716  cdleme10  40717  cdleme11c  40724  cdleme13  40735  cdleme15b  40738  cdleme15d  40740  cdleme15  40741  cdleme16b  40742  cdleme16e  40745  cdleme16f  40746  cdleme17b  40750  cdleme22gb  40757  cdlemedb  40760  cdlemednpq  40762  cdleme20zN  40764  cdleme19a  40766  cdleme19c  40768  cdleme20aN  40772  cdleme20c  40774  cdleme20d  40775  cdleme20e  40776  cdleme20j  40781  cdleme20l  40785  cdleme21c  40790  cdleme21ct  40792  cdleme22aa  40802  cdleme22b  40804  cdleme22cN  40805  cdleme22d  40806  cdleme22e  40807  cdleme22eALTN  40808  cdleme22f  40809  cdleme22g  40811  cdleme23a  40812  cdleme23b  40813  cdleme23c  40814  cdleme28a  40833  cdleme35a  40911  cdleme35fnpq  40912  cdleme35b  40913  cdleme35c  40914  cdleme35d  40915  cdleme35e  40916  cdleme35f  40917  cdleme42a  40934  cdleme42c  40935  cdleme42h  40945  cdleme42i  40946  cdlemeg46frv  40988  cdlemeg46vrg  40990  cdlemeg46rgv  40991  cdlemeg46req  40992  cdlemf1  41024  cdlemf2  41025  cdlemg2fv2  41063  cdlemg2m  41067  cdlemg4  41080  cdlemg8b  41091  cdlemg10bALTN  41099  cdlemg10c  41102  cdlemg10  41104  cdlemg12e  41110  cdlemg12f  41111  cdlemg12g  41112  cdlemg12  41113  cdlemg13a  41114  cdlemg17a  41124  cdlemg17dALTN  41127  cdlemg17h  41131  cdlemg17  41140  cdlemg18b  41142  cdlemg19a  41146  cdlemg19  41147  cdlemg27a  41155  cdlemg27b  41159  cdlemg31a  41160  cdlemg31b  41161  cdlemg33b0  41164  cdlemg33a  41169  trlcoabs2N  41185  trlcolem  41189  cdlemg42  41192  cdlemg46  41198  cdlemh1  41278  cdlemk3  41296  cdlemk10  41306  cdlemk12  41313  cdlemkole  41316  cdlemk14  41317  cdlemk15  41318  cdlemk1u  41322  cdlemk5u  41324  cdlemk12u  41335  cdlemk37  41377  cdlemk39  41379  cdlemkid1  41385  cdlemk51  41416  cdlemk52  41417  dia2dimlem1  41527  dia2dimlem2  41528  dia2dimlem3  41529  dia2dimlem10  41536  dia2dimlem12  41538  cdlemm10N  41581  cdlemn2  41658  cdlemn10  41669  dib2dim  41706  dih2dimb  41707  dih2dimbALTN  41708  dihjatcclem1  41881  dihjatcclem2  41882  dihjatcclem4  41884  dvh4dimat  41901