Theorem hlatjcl 39566

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6490  (class class class)co 7356  Basecbs 17134  joincjn 18232  Latclat 18352  Atomscatm 39462  HLchlt 39549

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-lub 18265  df-glb 18266  df-join 18267  df-meet 18268  df-lat 18353  df-ats 39466  df-atl 39497  df-cvlat 39521  df-hlat 39550

This theorem is referenced by:  atcvr0eq  39625  2atjm  39644  atbtwn  39645  3dim0  39656  3dimlem3a  39659  3dimlem3OLDN  39661  3dimlem4OLDN  39664  3dim3  39668  2dim  39669  ps-1  39676  hlatexch3N  39679  hlatexch4  39680  ps-2b  39681  3atlem1  39682  3atlem2  39683  llni2  39711  llnle  39717  2at0mat0  39724  2atm  39726  islpln5  39734  lplni2  39736  lplnnle2at  39740  2atnelpln  39743  islpln2a  39747  llncvrlpln2  39756  2atmat  39760  2llnjaN  39765  islvol5  39778  lvoli2  39780  lvolnle3at  39781  3atnelvolN  39785  islvol2aN  39791  4atlem0a  39792  4atlem3  39795  4atlem3a  39796  4atlem3b  39797  4atlem4a  39798  4atlem4b  39799  4atlem4c  39800  4atlem4d  39801  4atlem9  39802  4atlem10a  39803  4atlem10  39805  4atlem11a  39806  4atlem11b  39807  4atlem11  39808  4atlem12a  39809  4atlem12b  39810  4atlem12  39811  4at  39812  4at2  39813  lplncvrlvol2  39814  2lplnja  39818  dalempjqeb  39844  dalemsjteb  39845  dalemtjueb  39846  dalemply  39853  dalem1  39858  dalemcea  39859  dalem3  39863  dalem4  39864  dalem5  39866  dalem-cly  39870  dalem17  39879  dalem21  39893  dalem24  39896  dalem25  39897  dalem27  39898  dalem38  39909  dalem39  39910  dalem43  39914  dalem44  39915  dalem45  39916  dalem55  39926  dalem56  39927  dalem57  39928  2atm2atN  39984  2llnma1b  39985  2llnma3r  39987  llnmod2i2  40062  llnexchb2lem  40067  dalawlem1  40070  dalawlem2  40071  dalawlem3  40072  dalawlem4  40073  dalawlem5  40074  dalawlem6  40075  dalawlem7  40076  dalawlem8  40077  dalawlem9  40078  dalawlem11  40080  dalawlem12  40081  dalawlem15  40084  lhp2lt  40200  lhpexle2lem  40208  lhpexle3lem  40210  lhp2at0  40231  lhp2atnle  40232  lhpat3  40245  4atexlempsb  40259  4atexlemqtb  40260  4atexlemunv  40265  4atexlemtlw  40266  4atexlemc  40268  4atexlemnclw  40269  4atexlemcnd  40271  trlval3  40386  trlval4  40387  cdlemc4  40393  cdlemc5  40394  cdlemc6  40395  cdlemd2  40398  cdleme0e  40416  cdlemeulpq  40419  cdleme01N  40420  cdleme0ex1N  40422  cdleme3g  40433  cdleme3h  40434  cdleme3  40436  cdleme4  40437  cdleme4a  40438  cdleme5  40439  cdleme7aa  40441  cdleme7c  40444  cdleme7d  40445  cdleme7e  40446  cdleme7ga  40447  cdleme7  40448  cdleme9b  40451  cdleme9  40452  cdleme10  40453  cdleme11c  40460  cdleme13  40471  cdleme15b  40474  cdleme15d  40476  cdleme15  40477  cdleme16b  40478  cdleme16e  40481  cdleme16f  40482  cdleme17b  40486  cdleme22gb  40493  cdlemedb  40496  cdlemednpq  40498  cdleme20zN  40500  cdleme19a  40502  cdleme19c  40504  cdleme20aN  40508  cdleme20c  40510  cdleme20d  40511  cdleme20e  40512  cdleme20j  40517  cdleme20l  40521  cdleme21c  40526  cdleme21ct  40528  cdleme22aa  40538  cdleme22b  40540  cdleme22cN  40541  cdleme22d  40542  cdleme22e  40543  cdleme22eALTN  40544  cdleme22f  40545  cdleme22g  40547  cdleme23a  40548  cdleme23b  40549  cdleme23c  40550  cdleme28a  40569  cdleme35a  40647  cdleme35fnpq  40648  cdleme35b  40649  cdleme35c  40650  cdleme35d  40651  cdleme35e  40652  cdleme35f  40653  cdleme42a  40670  cdleme42c  40671  cdleme42h  40681  cdleme42i  40682  cdlemeg46frv  40724  cdlemeg46vrg  40726  cdlemeg46rgv  40727  cdlemeg46req  40728  cdlemf1  40760  cdlemf2  40761  cdlemg2fv2  40799  cdlemg2m  40803  cdlemg4  40816  cdlemg8b  40827  cdlemg10bALTN  40835  cdlemg10c  40838  cdlemg10  40840  cdlemg12e  40846  cdlemg12f  40847  cdlemg12g  40848  cdlemg12  40849  cdlemg13a  40850  cdlemg17a  40860  cdlemg17dALTN  40863  cdlemg17h  40867  cdlemg17  40876  cdlemg18b  40878  cdlemg19a  40882  cdlemg19  40883  cdlemg27a  40891  cdlemg27b  40895  cdlemg31a  40896  cdlemg31b  40897  cdlemg33b0  40900  cdlemg33a  40905  trlcoabs2N  40921  trlcolem  40925  cdlemg42  40928  cdlemg46  40934  cdlemh1  41014  cdlemk3  41032  cdlemk10  41042  cdlemk12  41049  cdlemkole  41052  cdlemk14  41053  cdlemk15  41054  cdlemk1u  41058  cdlemk5u  41060  cdlemk12u  41071  cdlemk37  41113  cdlemk39  41115  cdlemkid1  41121  cdlemk51  41152  cdlemk52  41153  dia2dimlem1  41263  dia2dimlem2  41264  dia2dimlem3  41265  dia2dimlem10  41272  dia2dimlem12  41274  cdlemm10N  41317  cdlemn2  41394  cdlemn10  41405  dib2dim  41442  dih2dimb  41443  dih2dimbALTN  41444  dihjatcclem1  41617  dihjatcclem2  41618  dihjatcclem4  41620  dvh4dimat  41637