Theorem hlatjcl 40243

Description: Closure of join operation. Frequently-used special case of latjcl 18530 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 40239	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 40165	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 40165	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18530	. 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 6533  (class class class)co 7414  Basecbs 17304  joincjn 18402  Latclat 18522  Atomscatm 40139  HLchlt 40226

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 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-lub 18435  df-glb 18436  df-join 18437  df-meet 18438  df-lat 18523  df-ats 40143  df-atl 40174  df-cvlat 40198  df-hlat 40227

This theorem is used by:  atcvr0eq  40302  2atjm  40321  atbtwn  40322  3dim0  40333  3dimlem3a  40336  3dimlem3OLDN  40338  3dimlem4OLDN  40341  3dim3  40345  2dim  40346  ps-1  40353  hlatexch3N  40356  hlatexch4  40357  ps-2b  40358  3atlem1  40359  3atlem2  40360  llni2  40388  llnle  40394  2at0mat0  40401  2atm  40403  islpln5  40411  lplni2  40413  lplnnle2at  40417  2atnelpln  40420  islpln2a  40424  llncvrlpln2  40433  2atmat  40437  2llnjaN  40442  islvol5  40455  lvoli2  40457  lvolnle3at  40458  3atnelvolN  40462  islvol2aN  40468  4atlem0a  40469  4atlem3  40472  4atlem3a  40473  4atlem3b  40474  4atlem4a  40475  4atlem4b  40476  4atlem4c  40477  4atlem4d  40478  4atlem9  40479  4atlem10a  40480  4atlem10  40482  4atlem11a  40483  4atlem11b  40484  4atlem11  40485  4atlem12a  40486  4atlem12b  40487  4atlem12  40488  4at  40489  4at2  40490  lplncvrlvol2  40491  2lplnja  40495  dalempjqeb  40521  dalemsjteb  40522  dalemtjueb  40523  dalemply  40530  dalem1  40535  dalemcea  40536  dalem3  40540  dalem4  40541  dalem5  40543  dalem-cly  40547  dalem17  40556  dalem21  40570  dalem24  40573  dalem25  40574  dalem27  40575  dalem38  40586  dalem39  40587  dalem43  40591  dalem44  40592  dalem45  40593  dalem55  40603  dalem56  40604  dalem57  40605  2atm2atN  40661  2llnma1b  40662  2llnma3r  40664  llnmod2i2  40739  llnexchb2lem  40744  dalawlem1  40747  dalawlem2  40748  dalawlem3  40749  dalawlem4  40750  dalawlem5  40751  dalawlem6  40752  dalawlem7  40753  dalawlem8  40754  dalawlem9  40755  dalawlem11  40757  dalawlem12  40758  dalawlem15  40761  lhp2lt  40877  lhpexle2lem  40885  lhpexle3lem  40887  lhp2at0  40908  lhp2atnle  40909  lhpat3  40922  4atexlempsb  40936  4atexlemqtb  40937  4atexlemunv  40942  4atexlemtlw  40943  4atexlemc  40945  4atexlemnclw  40946  4atexlemcnd  40948  trlval3  41063  trlval4  41064  cdlemc4  41070  cdlemc5  41071  cdlemc6  41072  cdlemd2  41075  cdleme0e  41093  cdlemeulpq  41096  cdleme01N  41097  cdleme0ex1N  41099  cdleme3g  41110  cdleme3h  41111  cdleme3  41113  cdleme4  41114  cdleme4a  41115  cdleme5  41116  cdleme7aa  41118  cdleme7c  41121  cdleme7d  41122  cdleme7e  41123  cdleme7ga  41124  cdleme7  41125  cdleme9b  41128  cdleme9  41129  cdleme10  41130  cdleme11c  41137  cdleme13  41148  cdleme15b  41151  cdleme15d  41153  cdleme15  41154  cdleme16b  41155  cdleme16e  41158  cdleme16f  41159  cdleme17b  41163  cdleme22gb  41170  cdlemedb  41173  cdlemednpq  41175  cdleme20zN  41177  cdleme19a  41179  cdleme19c  41181  cdleme20aN  41185  cdleme20c  41187  cdleme20d  41188  cdleme20e  41189  cdleme20j  41194  cdleme20l  41198  cdleme21c  41203  cdleme21ct  41205  cdleme22aa  41215  cdleme22b  41217  cdleme22cN  41218  cdleme22d  41219  cdleme22e  41220  cdleme22eALTN  41221  cdleme22f  41222  cdleme22g  41224  cdleme23a  41225  cdleme23b  41226  cdleme23c  41227  cdleme28a  41246  cdleme35a  41324  cdleme35fnpq  41325  cdleme35b  41326  cdleme35c  41327  cdleme35d  41328  cdleme35e  41329  cdleme35f  41330  cdleme42a  41347  cdleme42c  41348  cdleme42h  41358  cdleme42i  41359  cdlemeg46frv  41401  cdlemeg46vrg  41403  cdlemeg46rgv  41404  cdlemeg46req  41405  cdlemf1  41437  cdlemf2  41438  cdlemg2fv2  41476  cdlemg2m  41480  cdlemg4  41493  cdlemg8b  41504  cdlemg10bALTN  41512  cdlemg10c  41515  cdlemg10  41517  cdlemg12e  41523  cdlemg12f  41524  cdlemg12g  41525  cdlemg12  41526  cdlemg13a  41527  cdlemg17a  41537  cdlemg17dALTN  41540  cdlemg17h  41544  cdlemg17  41553  cdlemg18b  41555  cdlemg19a  41559  cdlemg19  41560  cdlemg27a  41568  cdlemg27b  41572  cdlemg31a  41573  cdlemg31b  41574  cdlemg33b0  41577  cdlemg33a  41582  trlcoabs2N  41598  trlcolem  41602  cdlemg42  41605  cdlemg46  41611  cdlemh1  41691  cdlemk3  41709  cdlemk10  41719  cdlemk12  41726  cdlemkole  41729  cdlemk14  41730  cdlemk15  41731  cdlemk1u  41735  cdlemk5u  41737  cdlemk12u  41748  cdlemk37  41790  cdlemk39  41792  cdlemkid1  41798  cdlemk51  41829  cdlemk52  41830  dia2dimlem1  41940  dia2dimlem2  41941  dia2dimlem3  41942  dia2dimlem10  41949  dia2dimlem12  41951  cdlemm10N  41994  cdlemn2  42071  cdlemn10  42082  dib2dim  42119  dih2dimb  42120  dih2dimbALTN  42121  dihjatcclem1  42294  dihjatcclem2  42295  dihjatcclem4  42297  dvh4dimat  42314