Theorem hlatjcl 40031

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ‘cfv 6537  (class class class)co 7411  Basecbs 17269  joincjn 18367  Latclat 18487  Atomscatm 39927  HLchlt 40014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-lub 18400  df-glb 18401  df-join 18402  df-meet 18403  df-lat 18488  df-ats 39931  df-atl 39962  df-cvlat 39986  df-hlat 40015

This theorem is referenced by:  atcvr0eq  40090  2atjm  40109  atbtwn  40110  3dim0  40121  3dimlem3a  40124  3dimlem3OLDN  40126  3dimlem4OLDN  40129  3dim3  40133  2dim  40134  ps-1  40141  hlatexch3N  40144  hlatexch4  40145  ps-2b  40146  3atlem1  40147  3atlem2  40148  llni2  40176  llnle  40182  2at0mat0  40189  2atm  40191  islpln5  40199  lplni2  40201  lplnnle2at  40205  2atnelpln  40208  islpln2a  40212  llncvrlpln2  40221  2atmat  40225  2llnjaN  40230  islvol5  40243  lvoli2  40245  lvolnle3at  40246  3atnelvolN  40250  islvol2aN  40256  4atlem0a  40257  4atlem3  40260  4atlem3a  40261  4atlem3b  40262  4atlem4a  40263  4atlem4b  40264  4atlem4c  40265  4atlem4d  40266  4atlem9  40267  4atlem10a  40268  4atlem10  40270  4atlem11a  40271  4atlem11b  40272  4atlem11  40273  4atlem12a  40274  4atlem12b  40275  4atlem12  40276  4at  40277  4at2  40278  lplncvrlvol2  40279  2lplnja  40283  dalempjqeb  40309  dalemsjteb  40310  dalemtjueb  40311  dalemply  40318  dalem1  40323  dalemcea  40324  dalem3  40328  dalem4  40329  dalem5  40331  dalem-cly  40335  dalem17  40344  dalem21  40358  dalem24  40361  dalem25  40362  dalem27  40363  dalem38  40374  dalem39  40375  dalem43  40379  dalem44  40380  dalem45  40381  dalem55  40391  dalem56  40392  dalem57  40393  2atm2atN  40449  2llnma1b  40450  2llnma3r  40452  llnmod2i2  40527  llnexchb2lem  40532  dalawlem1  40535  dalawlem2  40536  dalawlem3  40537  dalawlem4  40538  dalawlem5  40539  dalawlem6  40540  dalawlem7  40541  dalawlem8  40542  dalawlem9  40543  dalawlem11  40545  dalawlem12  40546  dalawlem15  40549  lhp2lt  40665  lhpexle2lem  40673  lhpexle3lem  40675  lhp2at0  40696  lhp2atnle  40697  lhpat3  40710  4atexlempsb  40724  4atexlemqtb  40725  4atexlemunv  40730  4atexlemtlw  40731  4atexlemc  40733  4atexlemnclw  40734  4atexlemcnd  40736  trlval3  40851  trlval4  40852  cdlemc4  40858  cdlemc5  40859  cdlemc6  40860  cdlemd2  40863  cdleme0e  40881  cdlemeulpq  40884  cdleme01N  40885  cdleme0ex1N  40887  cdleme3g  40898  cdleme3h  40899  cdleme3  40901  cdleme4  40902  cdleme4a  40903  cdleme5  40904  cdleme7aa  40906  cdleme7c  40909  cdleme7d  40910  cdleme7e  40911  cdleme7ga  40912  cdleme7  40913  cdleme9b  40916  cdleme9  40917  cdleme10  40918  cdleme11c  40925  cdleme13  40936  cdleme15b  40939  cdleme15d  40941  cdleme15  40942  cdleme16b  40943  cdleme16e  40946  cdleme16f  40947  cdleme17b  40951  cdleme22gb  40958  cdlemedb  40961  cdlemednpq  40963  cdleme20zN  40965  cdleme19a  40967  cdleme19c  40969  cdleme20aN  40973  cdleme20c  40975  cdleme20d  40976  cdleme20e  40977  cdleme20j  40982  cdleme20l  40986  cdleme21c  40991  cdleme21ct  40993  cdleme22aa  41003  cdleme22b  41005  cdleme22cN  41006  cdleme22d  41007  cdleme22e  41008  cdleme22eALTN  41009  cdleme22f  41010  cdleme22g  41012  cdleme23a  41013  cdleme23b  41014  cdleme23c  41015  cdleme28a  41034  cdleme35a  41112  cdleme35fnpq  41113  cdleme35b  41114  cdleme35c  41115  cdleme35d  41116  cdleme35e  41117  cdleme35f  41118  cdleme42a  41135  cdleme42c  41136  cdleme42h  41146  cdleme42i  41147  cdlemeg46frv  41189  cdlemeg46vrg  41191  cdlemeg46rgv  41192  cdlemeg46req  41193  cdlemf1  41225  cdlemf2  41226  cdlemg2fv2  41264  cdlemg2m  41268  cdlemg4  41281  cdlemg8b  41292  cdlemg10bALTN  41300  cdlemg10c  41303  cdlemg10  41305  cdlemg12e  41311  cdlemg12f  41312  cdlemg12g  41313  cdlemg12  41314  cdlemg13a  41315  cdlemg17a  41325  cdlemg17dALTN  41328  cdlemg17h  41332  cdlemg17  41341  cdlemg18b  41343  cdlemg19a  41347  cdlemg19  41348  cdlemg27a  41356  cdlemg27b  41360  cdlemg31a  41361  cdlemg31b  41362  cdlemg33b0  41365  cdlemg33a  41370  trlcoabs2N  41386  trlcolem  41390  cdlemg42  41393  cdlemg46  41399  cdlemh1  41479  cdlemk3  41497  cdlemk10  41507  cdlemk12  41514  cdlemkole  41517  cdlemk14  41518  cdlemk15  41519  cdlemk1u  41523  cdlemk5u  41525  cdlemk12u  41536  cdlemk37  41578  cdlemk39  41580  cdlemkid1  41586  cdlemk51  41617  cdlemk52  41618  dia2dimlem1  41728  dia2dimlem2  41729  dia2dimlem3  41730  dia2dimlem10  41737  dia2dimlem12  41739  cdlemm10N  41782  cdlemn2  41859  cdlemn10  41870  dib2dim  41907  dih2dimb  41908  dih2dimbALTN  41909  dihjatcclem1  42082  dihjatcclem2  42083  dihjatcclem4  42085  dvh4dimat  42102