Theorem hlatjcl 40424

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  joincjn 18485  Latclat 18605  Atomscatm 40320  HLchlt 40407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-lub 18518  df-glb 18519  df-join 18520  df-meet 18521  df-lat 18606  df-ats 40324  df-atl 40355  df-cvlat 40379  df-hlat 40408

This theorem is used by:  atcvr0eq  40483  2atjm  40502  atbtwn  40503  3dim0  40514  3dimlem3a  40517  3dimlem3OLDN  40519  3dimlem4OLDN  40522  3dim3  40526  2dim  40527  ps-1  40534  hlatexch3N  40537  hlatexch4  40538  ps-2b  40539  3atlem1  40540  3atlem2  40541  llni2  40569  llnle  40575  2at0mat0  40582  2atm  40584  islpln5  40592  lplni2  40594  lplnnle2at  40598  2atnelpln  40601  islpln2a  40605  llncvrlpln2  40614  2atmat  40618  2llnjaN  40623  islvol5  40636  lvoli2  40638  lvolnle3at  40639  3atnelvolN  40643  islvol2aN  40649  4atlem0a  40650  4atlem3  40653  4atlem3a  40654  4atlem3b  40655  4atlem4a  40656  4atlem4b  40657  4atlem4c  40658  4atlem4d  40659  4atlem9  40660  4atlem10a  40661  4atlem10  40663  4atlem11a  40664  4atlem11b  40665  4atlem11  40666  4atlem12a  40667  4atlem12b  40668  4atlem12  40669  4at  40670  4at2  40671  lplncvrlvol2  40672  2lplnja  40676  dalempjqeb  40702  dalemsjteb  40703  dalemtjueb  40704  dalemply  40711  dalem1  40716  dalemcea  40717  dalem3  40721  dalem4  40722  dalem5  40724  dalem-cly  40728  dalem17  40737  dalem21  40751  dalem24  40754  dalem25  40755  dalem27  40756  dalem38  40767  dalem39  40768  dalem43  40772  dalem44  40773  dalem45  40774  dalem55  40784  dalem56  40785  dalem57  40786  2atm2atN  40842  2llnma1b  40843  2llnma3r  40845  llnmod2i2  40920  llnexchb2lem  40925  dalawlem1  40928  dalawlem2  40929  dalawlem3  40930  dalawlem4  40931  dalawlem5  40932  dalawlem6  40933  dalawlem7  40934  dalawlem8  40935  dalawlem9  40936  dalawlem11  40938  dalawlem12  40939  dalawlem15  40942  lhp2lt  41058  lhpexle2lem  41066  lhpexle3lem  41068  lhp2at0  41089  lhp2atnle  41090  lhpat3  41103  4atexlempsb  41117  4atexlemqtb  41118  4atexlemunv  41123  4atexlemtlw  41124  4atexlemc  41126  4atexlemnclw  41127  4atexlemcnd  41129  trlval3  41244  trlval4  41245  cdlemc4  41251  cdlemc5  41252  cdlemc6  41253  cdlemd2  41256  cdleme0e  41274  cdlemeulpq  41277  cdleme01N  41278  cdleme0ex1N  41280  cdleme3g  41291  cdleme3h  41292  cdleme3  41294  cdleme4  41295  cdleme4a  41296  cdleme5  41297  cdleme7aa  41299  cdleme7c  41302  cdleme7d  41303  cdleme7e  41304  cdleme7ga  41305  cdleme7  41306  cdleme9b  41309  cdleme9  41310  cdleme10  41311  cdleme11c  41318  cdleme13  41329  cdleme15b  41332  cdleme15d  41334  cdleme15  41335  cdleme16b  41336  cdleme16e  41339  cdleme16f  41340  cdleme17b  41344  cdleme22gb  41351  cdlemedb  41354  cdlemednpq  41356  cdleme20zN  41358  cdleme19a  41360  cdleme19c  41362  cdleme20aN  41366  cdleme20c  41368  cdleme20d  41369  cdleme20e  41370  cdleme20j  41375  cdleme20l  41379  cdleme21c  41384  cdleme21ct  41386  cdleme22aa  41396  cdleme22b  41398  cdleme22cN  41399  cdleme22d  41400  cdleme22e  41401  cdleme22eALTN  41402  cdleme22f  41403  cdleme22g  41405  cdleme23a  41406  cdleme23b  41407  cdleme23c  41408  cdleme28a  41427  cdleme35a  41505  cdleme35fnpq  41506  cdleme35b  41507  cdleme35c  41508  cdleme35d  41509  cdleme35e  41510  cdleme35f  41511  cdleme42a  41528  cdleme42c  41529  cdleme42h  41539  cdleme42i  41540  cdlemeg46frv  41582  cdlemeg46vrg  41584  cdlemeg46rgv  41585  cdlemeg46req  41586  cdlemf1  41618  cdlemf2  41619  cdlemg2fv2  41657  cdlemg2m  41661  cdlemg4  41674  cdlemg8b  41685  cdlemg10bALTN  41693  cdlemg10c  41696  cdlemg10  41698  cdlemg12e  41704  cdlemg12f  41705  cdlemg12g  41706  cdlemg12  41707  cdlemg13a  41708  cdlemg17a  41718  cdlemg17dALTN  41721  cdlemg17h  41725  cdlemg17  41734  cdlemg18b  41736  cdlemg19a  41740  cdlemg19  41741  cdlemg27a  41749  cdlemg27b  41753  cdlemg31a  41754  cdlemg31b  41755  cdlemg33b0  41758  cdlemg33a  41763  trlcoabs2N  41779  trlcolem  41783  cdlemg42  41786  cdlemg46  41792  cdlemh1  41872  cdlemk3  41890  cdlemk10  41900  cdlemk12  41907  cdlemkole  41910  cdlemk14  41911  cdlemk15  41912  cdlemk1u  41916  cdlemk5u  41918  cdlemk12u  41929  cdlemk37  41971  cdlemk39  41973  cdlemkid1  41979  cdlemk51  42010  cdlemk52  42011  dia2dimlem1  42121  dia2dimlem2  42122  dia2dimlem3  42123  dia2dimlem10  42130  dia2dimlem12  42132  cdlemm10N  42175  cdlemn2  42252  cdlemn10  42263  dib2dim  42300  dih2dimb  42301  dih2dimbALTN  42302  dihjatcclem1  42475  dihjatcclem2  42476  dihjatcclem4  42478  dvh4dimat  42495