Theorem hlatjcl 39476

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  joincjn 18217  Latclat 18337  Atomscatm 39372  HLchlt 39459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-lub 18250  df-glb 18251  df-join 18252  df-meet 18253  df-lat 18338  df-ats 39376  df-atl 39407  df-cvlat 39431  df-hlat 39460

This theorem is referenced by:  atcvr0eq  39535  2atjm  39554  atbtwn  39555  3dim0  39566  3dimlem3a  39569  3dimlem3OLDN  39571  3dimlem4OLDN  39574  3dim3  39578  2dim  39579  ps-1  39586  hlatexch3N  39589  hlatexch4  39590  ps-2b  39591  3atlem1  39592  3atlem2  39593  llni2  39621  llnle  39627  2at0mat0  39634  2atm  39636  islpln5  39644  lplni2  39646  lplnnle2at  39650  2atnelpln  39653  islpln2a  39657  llncvrlpln2  39666  2atmat  39670  2llnjaN  39675  islvol5  39688  lvoli2  39690  lvolnle3at  39691  3atnelvolN  39695  islvol2aN  39701  4atlem0a  39702  4atlem3  39705  4atlem3a  39706  4atlem3b  39707  4atlem4a  39708  4atlem4b  39709  4atlem4c  39710  4atlem4d  39711  4atlem9  39712  4atlem10a  39713  4atlem10  39715  4atlem11a  39716  4atlem11b  39717  4atlem11  39718  4atlem12a  39719  4atlem12b  39720  4atlem12  39721  4at  39722  4at2  39723  lplncvrlvol2  39724  2lplnja  39728  dalempjqeb  39754  dalemsjteb  39755  dalemtjueb  39756  dalemply  39763  dalem1  39768  dalemcea  39769  dalem3  39773  dalem4  39774  dalem5  39776  dalem-cly  39780  dalem17  39789  dalem21  39803  dalem24  39806  dalem25  39807  dalem27  39808  dalem38  39819  dalem39  39820  dalem43  39824  dalem44  39825  dalem45  39826  dalem55  39836  dalem56  39837  dalem57  39838  2atm2atN  39894  2llnma1b  39895  2llnma3r  39897  llnmod2i2  39972  llnexchb2lem  39977  dalawlem1  39980  dalawlem2  39981  dalawlem3  39982  dalawlem4  39983  dalawlem5  39984  dalawlem6  39985  dalawlem7  39986  dalawlem8  39987  dalawlem9  39988  dalawlem11  39990  dalawlem12  39991  dalawlem15  39994  lhp2lt  40110  lhpexle2lem  40118  lhpexle3lem  40120  lhp2at0  40141  lhp2atnle  40142  lhpat3  40155  4atexlempsb  40169  4atexlemqtb  40170  4atexlemunv  40175  4atexlemtlw  40176  4atexlemc  40178  4atexlemnclw  40179  4atexlemcnd  40181  trlval3  40296  trlval4  40297  cdlemc4  40303  cdlemc5  40304  cdlemc6  40305  cdlemd2  40308  cdleme0e  40326  cdlemeulpq  40329  cdleme01N  40330  cdleme0ex1N  40332  cdleme3g  40343  cdleme3h  40344  cdleme3  40346  cdleme4  40347  cdleme4a  40348  cdleme5  40349  cdleme7aa  40351  cdleme7c  40354  cdleme7d  40355  cdleme7e  40356  cdleme7ga  40357  cdleme7  40358  cdleme9b  40361  cdleme9  40362  cdleme10  40363  cdleme11c  40370  cdleme13  40381  cdleme15b  40384  cdleme15d  40386  cdleme15  40387  cdleme16b  40388  cdleme16e  40391  cdleme16f  40392  cdleme17b  40396  cdleme22gb  40403  cdlemedb  40406  cdlemednpq  40408  cdleme20zN  40410  cdleme19a  40412  cdleme19c  40414  cdleme20aN  40418  cdleme20c  40420  cdleme20d  40421  cdleme20e  40422  cdleme20j  40427  cdleme20l  40431  cdleme21c  40436  cdleme21ct  40438  cdleme22aa  40448  cdleme22b  40450  cdleme22cN  40451  cdleme22d  40452  cdleme22e  40453  cdleme22eALTN  40454  cdleme22f  40455  cdleme22g  40457  cdleme23a  40458  cdleme23b  40459  cdleme23c  40460  cdleme28a  40479  cdleme35a  40557  cdleme35fnpq  40558  cdleme35b  40559  cdleme35c  40560  cdleme35d  40561  cdleme35e  40562  cdleme35f  40563  cdleme42a  40580  cdleme42c  40581  cdleme42h  40591  cdleme42i  40592  cdlemeg46frv  40634  cdlemeg46vrg  40636  cdlemeg46rgv  40637  cdlemeg46req  40638  cdlemf1  40670  cdlemf2  40671  cdlemg2fv2  40709  cdlemg2m  40713  cdlemg4  40726  cdlemg8b  40737  cdlemg10bALTN  40745  cdlemg10c  40748  cdlemg10  40750  cdlemg12e  40756  cdlemg12f  40757  cdlemg12g  40758  cdlemg12  40759  cdlemg13a  40760  cdlemg17a  40770  cdlemg17dALTN  40773  cdlemg17h  40777  cdlemg17  40786  cdlemg18b  40788  cdlemg19a  40792  cdlemg19  40793  cdlemg27a  40801  cdlemg27b  40805  cdlemg31a  40806  cdlemg31b  40807  cdlemg33b0  40810  cdlemg33a  40815  trlcoabs2N  40831  trlcolem  40835  cdlemg42  40838  cdlemg46  40844  cdlemh1  40924  cdlemk3  40942  cdlemk10  40952  cdlemk12  40959  cdlemkole  40962  cdlemk14  40963  cdlemk15  40964  cdlemk1u  40968  cdlemk5u  40970  cdlemk12u  40981  cdlemk37  41023  cdlemk39  41025  cdlemkid1  41031  cdlemk51  41062  cdlemk52  41063  dia2dimlem1  41173  dia2dimlem2  41174  dia2dimlem3  41175  dia2dimlem10  41182  dia2dimlem12  41184  cdlemm10N  41227  cdlemn2  41304  cdlemn10  41315  dib2dim  41352  dih2dimb  41353  dih2dimbALTN  41354  dihjatcclem1  41527  dihjatcclem2  41528  dihjatcclem4  41530  dvh4dimat  41547