Theorem hlatjcl 39360

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  joincjn 18272  Latclat 18390  Atomscatm 39256  HLchlt 39343

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 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-lub 18305  df-glb 18306  df-join 18307  df-meet 18308  df-lat 18391  df-ats 39260  df-atl 39291  df-cvlat 39315  df-hlat 39344

This theorem is referenced by:  atcvr0eq  39420  2atjm  39439  atbtwn  39440  3dim0  39451  3dimlem3a  39454  3dimlem3OLDN  39456  3dimlem4OLDN  39459  3dim3  39463  2dim  39464  ps-1  39471  hlatexch3N  39474  hlatexch4  39475  ps-2b  39476  3atlem1  39477  3atlem2  39478  llni2  39506  llnle  39512  2at0mat0  39519  2atm  39521  islpln5  39529  lplni2  39531  lplnnle2at  39535  2atnelpln  39538  islpln2a  39542  llncvrlpln2  39551  2atmat  39555  2llnjaN  39560  islvol5  39573  lvoli2  39575  lvolnle3at  39576  3atnelvolN  39580  islvol2aN  39586  4atlem0a  39587  4atlem3  39590  4atlem3a  39591  4atlem3b  39592  4atlem4a  39593  4atlem4b  39594  4atlem4c  39595  4atlem4d  39596  4atlem9  39597  4atlem10a  39598  4atlem10  39600  4atlem11a  39601  4atlem11b  39602  4atlem11  39603  4atlem12a  39604  4atlem12b  39605  4atlem12  39606  4at  39607  4at2  39608  lplncvrlvol2  39609  2lplnja  39613  dalempjqeb  39639  dalemsjteb  39640  dalemtjueb  39641  dalemply  39648  dalem1  39653  dalemcea  39654  dalem3  39658  dalem4  39659  dalem5  39661  dalem-cly  39665  dalem17  39674  dalem21  39688  dalem24  39691  dalem25  39692  dalem27  39693  dalem38  39704  dalem39  39705  dalem43  39709  dalem44  39710  dalem45  39711  dalem55  39721  dalem56  39722  dalem57  39723  2atm2atN  39779  2llnma1b  39780  2llnma3r  39782  llnmod2i2  39857  llnexchb2lem  39862  dalawlem1  39865  dalawlem2  39866  dalawlem3  39867  dalawlem4  39868  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  dalawlem15  39879  lhp2lt  39995  lhpexle2lem  40003  lhpexle3lem  40005  lhp2at0  40026  lhp2atnle  40027  lhpat3  40040  4atexlempsb  40054  4atexlemqtb  40055  4atexlemunv  40060  4atexlemtlw  40061  4atexlemc  40063  4atexlemnclw  40064  4atexlemcnd  40066  trlval3  40181  trlval4  40182  cdlemc4  40188  cdlemc5  40189  cdlemc6  40190  cdlemd2  40193  cdleme0e  40211  cdlemeulpq  40214  cdleme01N  40215  cdleme0ex1N  40217  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4  40232  cdleme4a  40233  cdleme5  40234  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme9b  40246  cdleme9  40247  cdleme10  40248  cdleme11c  40255  cdleme13  40266  cdleme15b  40269  cdleme15d  40271  cdleme15  40272  cdleme16b  40273  cdleme16e  40276  cdleme16f  40277  cdleme17b  40281  cdleme22gb  40288  cdlemedb  40291  cdlemednpq  40293  cdleme20zN  40295  cdleme19a  40297  cdleme19c  40299  cdleme20aN  40303  cdleme20c  40305  cdleme20d  40306  cdleme20e  40307  cdleme20j  40312  cdleme20l  40316  cdleme21c  40321  cdleme21ct  40323  cdleme22aa  40333  cdleme22b  40335  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme22g  40342  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme28a  40364  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme35f  40448  cdleme42a  40465  cdleme42c  40466  cdleme42h  40476  cdleme42i  40477  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemf1  40555  cdlemf2  40556  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg4  40611  cdlemg8b  40622  cdlemg10bALTN  40630  cdlemg10c  40633  cdlemg10  40635  cdlemg12e  40641  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg13a  40645  cdlemg17a  40655  cdlemg17dALTN  40658  cdlemg17h  40662  cdlemg17  40671  cdlemg18b  40673  cdlemg19a  40677  cdlemg19  40678  cdlemg27a  40686  cdlemg27b  40690  cdlemg31a  40691  cdlemg31b  40692  cdlemg33b0  40695  cdlemg33a  40700  trlcoabs2N  40716  trlcolem  40720  cdlemg42  40723  cdlemg46  40729  cdlemh1  40809  cdlemk3  40827  cdlemk10  40837  cdlemk12  40844  cdlemkole  40847  cdlemk14  40848  cdlemk15  40849  cdlemk1u  40853  cdlemk5u  40855  cdlemk12u  40866  cdlemk37  40908  cdlemk39  40910  cdlemkid1  40916  cdlemk51  40947  cdlemk52  40948  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  dia2dimlem10  41067  dia2dimlem12  41069  cdlemm10N  41112  cdlemn2  41189  cdlemn10  41200  dib2dim  41237  dih2dimb  41238  dih2dimbALTN  41239  dihjatcclem1  41412  dihjatcclem2  41413  dihjatcclem4  41415  dvh4dimat  41432