Theorem hlatjcl 40241

Description: Closure of join operation. Frequently-used special case of latjcl 18528 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 40237	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		hlatjcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		hlatjcl.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 40163	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵)
5	2, 3	atbase 40163	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵)
6		hlatjcl.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcl 18528	. 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 17302  joincjn 18400  Latclat 18520  Atomscatm 40137  HLchlt 40224

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 18433  df-glb 18434  df-join 18435  df-meet 18436  df-lat 18521  df-ats 40141  df-atl 40172  df-cvlat 40196  df-hlat 40225

This theorem is used by:  atcvr0eq  40300  2atjm  40319  atbtwn  40320  3dim0  40331  3dimlem3a  40334  3dimlem3OLDN  40336  3dimlem4OLDN  40339  3dim3  40343  2dim  40344  ps-1  40351  hlatexch3N  40354  hlatexch4  40355  ps-2b  40356  3atlem1  40357  3atlem2  40358  llni2  40386  llnle  40392  2at0mat0  40399  2atm  40401  islpln5  40409  lplni2  40411  lplnnle2at  40415  2atnelpln  40418  islpln2a  40422  llncvrlpln2  40431  2atmat  40435  2llnjaN  40440  islvol5  40453  lvoli2  40455  lvolnle3at  40456  3atnelvolN  40460  islvol2aN  40466  4atlem0a  40467  4atlem3  40470  4atlem3a  40471  4atlem3b  40472  4atlem4a  40473  4atlem4b  40474  4atlem4c  40475  4atlem4d  40476  4atlem9  40477  4atlem10a  40478  4atlem10  40480  4atlem11a  40481  4atlem11b  40482  4atlem11  40483  4atlem12a  40484  4atlem12b  40485  4atlem12  40486  4at  40487  4at2  40488  lplncvrlvol2  40489  2lplnja  40493  dalempjqeb  40519  dalemsjteb  40520  dalemtjueb  40521  dalemply  40528  dalem1  40533  dalemcea  40534  dalem3  40538  dalem4  40539  dalem5  40541  dalem-cly  40545  dalem17  40554  dalem21  40568  dalem24  40571  dalem25  40572  dalem27  40573  dalem38  40584  dalem39  40585  dalem43  40589  dalem44  40590  dalem45  40591  dalem55  40601  dalem56  40602  dalem57  40603  2atm2atN  40659  2llnma1b  40660  2llnma3r  40662  llnmod2i2  40737  llnexchb2lem  40742  dalawlem1  40745  dalawlem2  40746  dalawlem3  40747  dalawlem4  40748  dalawlem5  40749  dalawlem6  40750  dalawlem7  40751  dalawlem8  40752  dalawlem9  40753  dalawlem11  40755  dalawlem12  40756  dalawlem15  40759  lhp2lt  40875  lhpexle2lem  40883  lhpexle3lem  40885  lhp2at0  40906  lhp2atnle  40907  lhpat3  40920  4atexlempsb  40934  4atexlemqtb  40935  4atexlemunv  40940  4atexlemtlw  40941  4atexlemc  40943  4atexlemnclw  40944  4atexlemcnd  40946  trlval3  41061  trlval4  41062  cdlemc4  41068  cdlemc5  41069  cdlemc6  41070  cdlemd2  41073  cdleme0e  41091  cdlemeulpq  41094  cdleme01N  41095  cdleme0ex1N  41097  cdleme3g  41108  cdleme3h  41109  cdleme3  41111  cdleme4  41112  cdleme4a  41113  cdleme5  41114  cdleme7aa  41116  cdleme7c  41119  cdleme7d  41120  cdleme7e  41121  cdleme7ga  41122  cdleme7  41123  cdleme9b  41126  cdleme9  41127  cdleme10  41128  cdleme11c  41135  cdleme13  41146  cdleme15b  41149  cdleme15d  41151  cdleme15  41152  cdleme16b  41153  cdleme16e  41156  cdleme16f  41157  cdleme17b  41161  cdleme22gb  41168  cdlemedb  41171  cdlemednpq  41173  cdleme20zN  41175  cdleme19a  41177  cdleme19c  41179  cdleme20aN  41183  cdleme20c  41185  cdleme20d  41186  cdleme20e  41187  cdleme20j  41192  cdleme20l  41196  cdleme21c  41201  cdleme21ct  41203  cdleme22aa  41213  cdleme22b  41215  cdleme22cN  41216  cdleme22d  41217  cdleme22e  41218  cdleme22eALTN  41219  cdleme22f  41220  cdleme22g  41222  cdleme23a  41223  cdleme23b  41224  cdleme23c  41225  cdleme28a  41244  cdleme35a  41322  cdleme35fnpq  41323  cdleme35b  41324  cdleme35c  41325  cdleme35d  41326  cdleme35e  41327  cdleme35f  41328  cdleme42a  41345  cdleme42c  41346  cdleme42h  41356  cdleme42i  41357  cdlemeg46frv  41399  cdlemeg46vrg  41401  cdlemeg46rgv  41402  cdlemeg46req  41403  cdlemf1  41435  cdlemf2  41436  cdlemg2fv2  41474  cdlemg2m  41478  cdlemg4  41491  cdlemg8b  41502  cdlemg10bALTN  41510  cdlemg10c  41513  cdlemg10  41515  cdlemg12e  41521  cdlemg12f  41522  cdlemg12g  41523  cdlemg12  41524  cdlemg13a  41525  cdlemg17a  41535  cdlemg17dALTN  41538  cdlemg17h  41542  cdlemg17  41551  cdlemg18b  41553  cdlemg19a  41557  cdlemg19  41558  cdlemg27a  41566  cdlemg27b  41570  cdlemg31a  41571  cdlemg31b  41572  cdlemg33b0  41575  cdlemg33a  41580  trlcoabs2N  41596  trlcolem  41600  cdlemg42  41603  cdlemg46  41609  cdlemh1  41689  cdlemk3  41707  cdlemk10  41717  cdlemk12  41724  cdlemkole  41727  cdlemk14  41728  cdlemk15  41729  cdlemk1u  41733  cdlemk5u  41735  cdlemk12u  41746  cdlemk37  41788  cdlemk39  41790  cdlemkid1  41796  cdlemk51  41827  cdlemk52  41828  dia2dimlem1  41938  dia2dimlem2  41939  dia2dimlem3  41940  dia2dimlem10  41947  dia2dimlem12  41949  cdlemm10N  41992  cdlemn2  42069  cdlemn10  42080  dib2dim  42117  dih2dimb  42118  dih2dimbALTN  42119  dihjatcclem1  42292  dihjatcclem2  42293  dihjatcclem4  42295  dvh4dimat  42312