Theorem hlatjcl 39353

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  joincjn 18252  Latclat 18372  Atomscatm 39249  HLchlt 39336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-lub 18285  df-glb 18286  df-join 18287  df-meet 18288  df-lat 18373  df-ats 39253  df-atl 39284  df-cvlat 39308  df-hlat 39337

This theorem is referenced by:  atcvr0eq  39413  2atjm  39432  atbtwn  39433  3dim0  39444  3dimlem3a  39447  3dimlem3OLDN  39449  3dimlem4OLDN  39452  3dim3  39456  2dim  39457  ps-1  39464  hlatexch3N  39467  hlatexch4  39468  ps-2b  39469  3atlem1  39470  3atlem2  39471  llni2  39499  llnle  39505  2at0mat0  39512  2atm  39514  islpln5  39522  lplni2  39524  lplnnle2at  39528  2atnelpln  39531  islpln2a  39535  llncvrlpln2  39544  2atmat  39548  2llnjaN  39553  islvol5  39566  lvoli2  39568  lvolnle3at  39569  3atnelvolN  39573  islvol2aN  39579  4atlem0a  39580  4atlem3  39583  4atlem3a  39584  4atlem3b  39585  4atlem4a  39586  4atlem4b  39587  4atlem4c  39588  4atlem4d  39589  4atlem9  39590  4atlem10a  39591  4atlem10  39593  4atlem11a  39594  4atlem11b  39595  4atlem11  39596  4atlem12a  39597  4atlem12b  39598  4atlem12  39599  4at  39600  4at2  39601  lplncvrlvol2  39602  2lplnja  39606  dalempjqeb  39632  dalemsjteb  39633  dalemtjueb  39634  dalemply  39641  dalem1  39646  dalemcea  39647  dalem3  39651  dalem4  39652  dalem5  39654  dalem-cly  39658  dalem17  39667  dalem21  39681  dalem24  39684  dalem25  39685  dalem27  39686  dalem38  39697  dalem39  39698  dalem43  39702  dalem44  39703  dalem45  39704  dalem55  39714  dalem56  39715  dalem57  39716  2atm2atN  39772  2llnma1b  39773  2llnma3r  39775  llnmod2i2  39850  llnexchb2lem  39855  dalawlem1  39858  dalawlem2  39859  dalawlem3  39860  dalawlem4  39861  dalawlem5  39862  dalawlem6  39863  dalawlem7  39864  dalawlem8  39865  dalawlem9  39866  dalawlem11  39868  dalawlem12  39869  dalawlem15  39872  lhp2lt  39988  lhpexle2lem  39996  lhpexle3lem  39998  lhp2at0  40019  lhp2atnle  40020  lhpat3  40033  4atexlempsb  40047  4atexlemqtb  40048  4atexlemunv  40053  4atexlemtlw  40054  4atexlemc  40056  4atexlemnclw  40057  4atexlemcnd  40059  trlval3  40174  trlval4  40175  cdlemc4  40181  cdlemc5  40182  cdlemc6  40183  cdlemd2  40186  cdleme0e  40204  cdlemeulpq  40207  cdleme01N  40208  cdleme0ex1N  40210  cdleme3g  40221  cdleme3h  40222  cdleme3  40224  cdleme4  40225  cdleme4a  40226  cdleme5  40227  cdleme7aa  40229  cdleme7c  40232  cdleme7d  40233  cdleme7e  40234  cdleme7ga  40235  cdleme7  40236  cdleme9b  40239  cdleme9  40240  cdleme10  40241  cdleme11c  40248  cdleme13  40259  cdleme15b  40262  cdleme15d  40264  cdleme15  40265  cdleme16b  40266  cdleme16e  40269  cdleme16f  40270  cdleme17b  40274  cdleme22gb  40281  cdlemedb  40284  cdlemednpq  40286  cdleme20zN  40288  cdleme19a  40290  cdleme19c  40292  cdleme20aN  40296  cdleme20c  40298  cdleme20d  40299  cdleme20e  40300  cdleme20j  40305  cdleme20l  40309  cdleme21c  40314  cdleme21ct  40316  cdleme22aa  40326  cdleme22b  40328  cdleme22cN  40329  cdleme22d  40330  cdleme22e  40331  cdleme22eALTN  40332  cdleme22f  40333  cdleme22g  40335  cdleme23a  40336  cdleme23b  40337  cdleme23c  40338  cdleme28a  40357  cdleme35a  40435  cdleme35fnpq  40436  cdleme35b  40437  cdleme35c  40438  cdleme35d  40439  cdleme35e  40440  cdleme35f  40441  cdleme42a  40458  cdleme42c  40459  cdleme42h  40469  cdleme42i  40470  cdlemeg46frv  40512  cdlemeg46vrg  40514  cdlemeg46rgv  40515  cdlemeg46req  40516  cdlemf1  40548  cdlemf2  40549  cdlemg2fv2  40587  cdlemg2m  40591  cdlemg4  40604  cdlemg8b  40615  cdlemg10bALTN  40623  cdlemg10c  40626  cdlemg10  40628  cdlemg12e  40634  cdlemg12f  40635  cdlemg12g  40636  cdlemg12  40637  cdlemg13a  40638  cdlemg17a  40648  cdlemg17dALTN  40651  cdlemg17h  40655  cdlemg17  40664  cdlemg18b  40666  cdlemg19a  40670  cdlemg19  40671  cdlemg27a  40679  cdlemg27b  40683  cdlemg31a  40684  cdlemg31b  40685  cdlemg33b0  40688  cdlemg33a  40693  trlcoabs2N  40709  trlcolem  40713  cdlemg42  40716  cdlemg46  40722  cdlemh1  40802  cdlemk3  40820  cdlemk10  40830  cdlemk12  40837  cdlemkole  40840  cdlemk14  40841  cdlemk15  40842  cdlemk1u  40846  cdlemk5u  40848  cdlemk12u  40859  cdlemk37  40901  cdlemk39  40903  cdlemkid1  40909  cdlemk51  40940  cdlemk52  40941  dia2dimlem1  41051  dia2dimlem2  41052  dia2dimlem3  41053  dia2dimlem10  41060  dia2dimlem12  41062  cdlemm10N  41105  cdlemn2  41182  cdlemn10  41193  dib2dim  41230  dih2dimb  41231  dih2dimbALTN  41232  dihjatcclem1  41405  dihjatcclem2  41406  dihjatcclem4  41408  dvh4dimat  41425