Theorem hlatjcl 36518

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  joincjn 17554  Latclat 17655  Atomscatm 36414  HLchlt 36501

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-lub 17584  df-glb 17585  df-join 17586  df-meet 17587  df-lat 17656  df-ats 36418  df-atl 36449  df-cvlat 36473  df-hlat 36502

This theorem is referenced by:  atcvr0eq  36577  2atjm  36596  atbtwn  36597  3dim0  36608  3dimlem3a  36611  3dimlem3OLDN  36613  3dimlem4OLDN  36616  3dim3  36620  2dim  36621  ps-1  36628  hlatexch3N  36631  hlatexch4  36632  ps-2b  36633  3atlem1  36634  3atlem2  36635  llni2  36663  llnle  36669  2at0mat0  36676  2atm  36678  islpln5  36686  lplni2  36688  lplnnle2at  36692  2atnelpln  36695  islpln2a  36699  llncvrlpln2  36708  2atmat  36712  2llnjaN  36717  islvol5  36730  lvoli2  36732  lvolnle3at  36733  3atnelvolN  36737  islvol2aN  36743  4atlem0a  36744  4atlem3  36747  4atlem3a  36748  4atlem3b  36749  4atlem4a  36750  4atlem4b  36751  4atlem4c  36752  4atlem4d  36753  4atlem9  36754  4atlem10a  36755  4atlem10  36757  4atlem11a  36758  4atlem11b  36759  4atlem11  36760  4atlem12a  36761  4atlem12b  36762  4atlem12  36763  4at  36764  4at2  36765  lplncvrlvol2  36766  2lplnja  36770  dalempjqeb  36796  dalemsjteb  36797  dalemtjueb  36798  dalemply  36805  dalem1  36810  dalemcea  36811  dalem3  36815  dalem4  36816  dalem5  36818  dalem-cly  36822  dalem17  36831  dalem21  36845  dalem24  36848  dalem25  36849  dalem27  36850  dalem38  36861  dalem39  36862  dalem43  36866  dalem44  36867  dalem45  36868  dalem55  36878  dalem56  36879  dalem57  36880  2atm2atN  36936  2llnma1b  36937  2llnma3r  36939  llnmod2i2  37014  llnexchb2lem  37019  dalawlem1  37022  dalawlem2  37023  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem15  37036  lhp2lt  37152  lhpexle2lem  37160  lhpexle3lem  37162  lhp2at0  37183  lhp2atnle  37184  lhpat3  37197  4atexlempsb  37211  4atexlemqtb  37212  4atexlemunv  37217  4atexlemtlw  37218  4atexlemc  37220  4atexlemnclw  37221  4atexlemcnd  37223  trlval3  37338  trlval4  37339  cdlemc4  37345  cdlemc5  37346  cdlemc6  37347  cdlemd2  37350  cdleme0e  37368  cdlemeulpq  37371  cdleme01N  37372  cdleme0ex1N  37374  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme4  37389  cdleme4a  37390  cdleme5  37391  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme9b  37403  cdleme9  37404  cdleme10  37405  cdleme11c  37412  cdleme13  37423  cdleme15b  37426  cdleme15d  37428  cdleme15  37429  cdleme16b  37430  cdleme16e  37433  cdleme16f  37434  cdleme17b  37438  cdleme22gb  37445  cdlemedb  37448  cdlemednpq  37450  cdleme20zN  37452  cdleme19a  37454  cdleme19c  37456  cdleme20aN  37460  cdleme20c  37462  cdleme20d  37463  cdleme20e  37464  cdleme20j  37469  cdleme20l  37473  cdleme21c  37478  cdleme21ct  37480  cdleme22aa  37490  cdleme22b  37492  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme22g  37499  cdleme23a  37500  cdleme23b  37501  cdleme23c  37502  cdleme28a  37521  cdleme35a  37599  cdleme35fnpq  37600  cdleme35b  37601  cdleme35c  37602  cdleme35d  37603  cdleme35e  37604  cdleme35f  37605  cdleme42a  37622  cdleme42c  37623  cdleme42h  37633  cdleme42i  37634  cdlemeg46frv  37676  cdlemeg46vrg  37678  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemf1  37712  cdlemf2  37713  cdlemg2fv2  37751  cdlemg2m  37755  cdlemg4  37768  cdlemg8b  37779  cdlemg10bALTN  37787  cdlemg10c  37790  cdlemg10  37792  cdlemg12e  37798  cdlemg12f  37799  cdlemg12g  37800  cdlemg12  37801  cdlemg13a  37802  cdlemg17a  37812  cdlemg17dALTN  37815  cdlemg17h  37819  cdlemg17  37828  cdlemg18b  37830  cdlemg19a  37834  cdlemg19  37835  cdlemg27a  37843  cdlemg27b  37847  cdlemg31a  37848  cdlemg31b  37849  cdlemg33b0  37852  cdlemg33a  37857  trlcoabs2N  37873  trlcolem  37877  cdlemg42  37880  cdlemg46  37886  cdlemh1  37966  cdlemk3  37984  cdlemk10  37994  cdlemk12  38001  cdlemkole  38004  cdlemk14  38005  cdlemk15  38006  cdlemk1u  38010  cdlemk5u  38012  cdlemk12u  38023  cdlemk37  38065  cdlemk39  38067  cdlemkid1  38073  cdlemk51  38104  cdlemk52  38105  dia2dimlem1  38215  dia2dimlem2  38216  dia2dimlem3  38217  dia2dimlem10  38224  dia2dimlem12  38226  cdlemm10N  38269  cdlemn2  38346  cdlemn10  38357  dib2dim  38394  dih2dimb  38395  dih2dimbALTN  38396  dihjatcclem1  38569  dihjatcclem2  38570  dihjatcclem4  38572  dvh4dimat  38589