Theorem hlatjcl 33671

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

Syntax hints:   → wi 4   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  joincjn 16767  Latclat 16868  Atomscatm 33568  HLchlt 33655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-lub 16797  df-glb 16798  df-join 16799  df-meet 16800  df-lat 16869  df-ats 33572  df-atl 33603  df-cvlat 33627  df-hlat 33656

This theorem is referenced by:  atcvr0eq  33730  2atjm  33749  atbtwn  33750  3dim0  33761  3dimlem3a  33764  3dimlem3OLDN  33766  3dimlem4OLDN  33769  3dim3  33773  2dim  33774  ps-1  33781  hlatexch3N  33784  hlatexch4  33785  ps-2b  33786  3atlem1  33787  3atlem2  33788  llni2  33816  llnle  33822  2at0mat0  33829  2atm  33831  islpln5  33839  lplni2  33841  lplnnle2at  33845  2atnelpln  33848  islpln2a  33852  llncvrlpln2  33861  2atmat  33865  2llnjaN  33870  islvol5  33883  lvoli2  33885  lvolnle3at  33886  3atnelvolN  33890  islvol2aN  33896  4atlem0a  33897  4atlem3  33900  4atlem3a  33901  4atlem3b  33902  4atlem4a  33903  4atlem4b  33904  4atlem4c  33905  4atlem4d  33906  4atlem9  33907  4atlem10a  33908  4atlem10  33910  4atlem11a  33911  4atlem11b  33912  4atlem11  33913  4atlem12a  33914  4atlem12b  33915  4atlem12  33916  4at  33917  4at2  33918  lplncvrlvol2  33919  2lplnja  33923  dalempjqeb  33949  dalemsjteb  33950  dalemtjueb  33951  dalemply  33958  dalem1  33963  dalemcea  33964  dalem3  33968  dalem4  33969  dalem5  33971  dalem-cly  33975  dalem17  33984  dalem21  33998  dalem24  34001  dalem25  34002  dalem27  34003  dalem38  34014  dalem39  34015  dalem43  34019  dalem44  34020  dalem45  34021  dalem55  34031  dalem56  34032  dalem57  34033  2atm2atN  34089  2llnma1b  34090  2llnma3r  34092  llnmod2i2  34167  llnexchb2lem  34172  dalawlem1  34175  dalawlem2  34176  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  dalawlem15  34189  lhp2lt  34305  lhpexle2lem  34313  lhpexle3lem  34315  lhp2at0  34336  lhp2atnle  34337  lhpat3  34350  4atexlempsb  34364  4atexlemqtb  34365  4atexlemunv  34370  4atexlemtlw  34371  4atexlemc  34373  4atexlemnclw  34374  4atexlemcnd  34376  trlval3  34492  trlval4  34493  cdlemc4  34499  cdlemc5  34500  cdlemc6  34501  cdlemd2  34504  cdleme0e  34522  cdlemeulpq  34525  cdleme01N  34526  cdleme0ex1N  34528  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4  34543  cdleme4a  34544  cdleme5  34545  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme9b  34557  cdleme9  34558  cdleme10  34559  cdleme11c  34566  cdleme13  34577  cdleme15b  34580  cdleme15d  34582  cdleme15  34583  cdleme16b  34584  cdleme16e  34587  cdleme16f  34588  cdleme17b  34592  cdleme22gb  34599  cdlemedb  34602  cdlemednpq  34604  cdleme20zN  34606  cdleme20yOLD  34608  cdleme19a  34609  cdleme19c  34611  cdleme20aN  34615  cdleme20c  34617  cdleme20d  34618  cdleme20e  34619  cdleme20j  34624  cdleme20l  34628  cdleme21c  34633  cdleme21ct  34635  cdleme22aa  34645  cdleme22b  34647  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme22g  34654  cdleme23a  34655  cdleme23b  34656  cdleme23c  34657  cdleme28a  34676  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35e  34759  cdleme35f  34760  cdleme42a  34777  cdleme42c  34778  cdleme42h  34788  cdleme42i  34789  cdlemeg46frv  34831  cdlemeg46vrg  34833  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemf1  34867  cdlemf2  34868  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg4  34923  cdlemg8b  34934  cdlemg10bALTN  34942  cdlemg10c  34945  cdlemg10  34947  cdlemg12e  34953  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg17a  34967  cdlemg17dALTN  34970  cdlemg17h  34974  cdlemg17  34983  cdlemg18b  34985  cdlemg19a  34989  cdlemg19  34990  cdlemg27a  34998  cdlemg27b  35002  cdlemg31a  35003  cdlemg31b  35004  cdlemg33b0  35007  cdlemg33a  35012  trlcoabs2N  35028  trlcolem  35032  cdlemg42  35035  cdlemg46  35041  cdlemh1  35121  cdlemk3  35139  cdlemk10  35149  cdlemk12  35156  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk1u  35165  cdlemk5u  35167  cdlemk12u  35178  cdlemk37  35220  cdlemk39  35222  cdlemkid1  35228  cdlemk51  35259  cdlemk52  35260  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  dia2dimlem10  35380  dia2dimlem12  35382  cdlemm10N  35425  cdlemn2  35502  cdlemn10  35513  dib2dim  35550  dih2dimb  35551  dih2dimbALTN  35552  dihjatcclem1  35725  dihjatcclem2  35726  dihjatcclem4  35728  dvh4dimat  35745