Theorem hlatjcl 36507

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113  ‘cfv 6358  (class class class)co 7159  Basecbs 16486  joincjn 17557  Latclat 17658  Atomscatm 36403  HLchlt 36490

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7117  df-ov 7162  df-oprab 7163  df-lub 17587  df-glb 17588  df-join 17589  df-meet 17590  df-lat 17659  df-ats 36407  df-atl 36438  df-cvlat 36462  df-hlat 36491

This theorem is referenced by:  atcvr0eq  36566  2atjm  36585  atbtwn  36586  3dim0  36597  3dimlem3a  36600  3dimlem3OLDN  36602  3dimlem4OLDN  36605  3dim3  36609  2dim  36610  ps-1  36617  hlatexch3N  36620  hlatexch4  36621  ps-2b  36622  3atlem1  36623  3atlem2  36624  llni2  36652  llnle  36658  2at0mat0  36665  2atm  36667  islpln5  36675  lplni2  36677  lplnnle2at  36681  2atnelpln  36684  islpln2a  36688  llncvrlpln2  36697  2atmat  36701  2llnjaN  36706  islvol5  36719  lvoli2  36721  lvolnle3at  36722  3atnelvolN  36726  islvol2aN  36732  4atlem0a  36733  4atlem3  36736  4atlem3a  36737  4atlem3b  36738  4atlem4a  36739  4atlem4b  36740  4atlem4c  36741  4atlem4d  36742  4atlem9  36743  4atlem10a  36744  4atlem10  36746  4atlem11a  36747  4atlem11b  36748  4atlem11  36749  4atlem12a  36750  4atlem12b  36751  4atlem12  36752  4at  36753  4at2  36754  lplncvrlvol2  36755  2lplnja  36759  dalempjqeb  36785  dalemsjteb  36786  dalemtjueb  36787  dalemply  36794  dalem1  36799  dalemcea  36800  dalem3  36804  dalem4  36805  dalem5  36807  dalem-cly  36811  dalem17  36820  dalem21  36834  dalem24  36837  dalem25  36838  dalem27  36839  dalem38  36850  dalem39  36851  dalem43  36855  dalem44  36856  dalem45  36857  dalem55  36867  dalem56  36868  dalem57  36869  2atm2atN  36925  2llnma1b  36926  2llnma3r  36928  llnmod2i2  37003  llnexchb2lem  37008  dalawlem1  37011  dalawlem2  37012  dalawlem3  37013  dalawlem4  37014  dalawlem5  37015  dalawlem6  37016  dalawlem7  37017  dalawlem8  37018  dalawlem9  37019  dalawlem11  37021  dalawlem12  37022  dalawlem15  37025  lhp2lt  37141  lhpexle2lem  37149  lhpexle3lem  37151  lhp2at0  37172  lhp2atnle  37173  lhpat3  37186  4atexlempsb  37200  4atexlemqtb  37201  4atexlemunv  37206  4atexlemtlw  37207  4atexlemc  37209  4atexlemnclw  37210  4atexlemcnd  37212  trlval3  37327  trlval4  37328  cdlemc4  37334  cdlemc5  37335  cdlemc6  37336  cdlemd2  37339  cdleme0e  37357  cdlemeulpq  37360  cdleme01N  37361  cdleme0ex1N  37363  cdleme3g  37374  cdleme3h  37375  cdleme3  37377  cdleme4  37378  cdleme4a  37379  cdleme5  37380  cdleme7aa  37382  cdleme7c  37385  cdleme7d  37386  cdleme7e  37387  cdleme7ga  37388  cdleme7  37389  cdleme9b  37392  cdleme9  37393  cdleme10  37394  cdleme11c  37401  cdleme13  37412  cdleme15b  37415  cdleme15d  37417  cdleme15  37418  cdleme16b  37419  cdleme16e  37422  cdleme16f  37423  cdleme17b  37427  cdleme22gb  37434  cdlemedb  37437  cdlemednpq  37439  cdleme20zN  37441  cdleme19a  37443  cdleme19c  37445  cdleme20aN  37449  cdleme20c  37451  cdleme20d  37452  cdleme20e  37453  cdleme20j  37458  cdleme20l  37462  cdleme21c  37467  cdleme21ct  37469  cdleme22aa  37479  cdleme22b  37481  cdleme22cN  37482  cdleme22d  37483  cdleme22e  37484  cdleme22eALTN  37485  cdleme22f  37486  cdleme22g  37488  cdleme23a  37489  cdleme23b  37490  cdleme23c  37491  cdleme28a  37510  cdleme35a  37588  cdleme35fnpq  37589  cdleme35b  37590  cdleme35c  37591  cdleme35d  37592  cdleme35e  37593  cdleme35f  37594  cdleme42a  37611  cdleme42c  37612  cdleme42h  37622  cdleme42i  37623  cdlemeg46frv  37665  cdlemeg46vrg  37667  cdlemeg46rgv  37668  cdlemeg46req  37669  cdlemf1  37701  cdlemf2  37702  cdlemg2fv2  37740  cdlemg2m  37744  cdlemg4  37757  cdlemg8b  37768  cdlemg10bALTN  37776  cdlemg10c  37779  cdlemg10  37781  cdlemg12e  37787  cdlemg12f  37788  cdlemg12g  37789  cdlemg12  37790  cdlemg13a  37791  cdlemg17a  37801  cdlemg17dALTN  37804  cdlemg17h  37808  cdlemg17  37817  cdlemg18b  37819  cdlemg19a  37823  cdlemg19  37824  cdlemg27a  37832  cdlemg27b  37836  cdlemg31a  37837  cdlemg31b  37838  cdlemg33b0  37841  cdlemg33a  37846  trlcoabs2N  37862  trlcolem  37866  cdlemg42  37869  cdlemg46  37875  cdlemh1  37955  cdlemk3  37973  cdlemk10  37983  cdlemk12  37990  cdlemkole  37993  cdlemk14  37994  cdlemk15  37995  cdlemk1u  37999  cdlemk5u  38001  cdlemk12u  38012  cdlemk37  38054  cdlemk39  38056  cdlemkid1  38062  cdlemk51  38093  cdlemk52  38094  dia2dimlem1  38204  dia2dimlem2  38205  dia2dimlem3  38206  dia2dimlem10  38213  dia2dimlem12  38215  cdlemm10N  38258  cdlemn2  38335  cdlemn10  38346  dib2dim  38383  dih2dimb  38384  dih2dimbALTN  38385  dihjatcclem1  38558  dihjatcclem2  38559  dihjatcclem4  38561  dvh4dimat  38578