Theorem hlatjcl 40201

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  (class class class)co 7419  Basecbs 17293  joincjn 18391  Latclat 18511  Atomscatm 40097  HLchlt 40184

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-lub 18424  df-glb 18425  df-join 18426  df-meet 18427  df-lat 18512  df-ats 40101  df-atl 40132  df-cvlat 40156  df-hlat 40185

This theorem is used by:  atcvr0eq  40260  2atjm  40279  atbtwn  40280  3dim0  40291  3dimlem3a  40294  3dimlem3OLDN  40296  3dimlem4OLDN  40299  3dim3  40303  2dim  40304  ps-1  40311  hlatexch3N  40314  hlatexch4  40315  ps-2b  40316  3atlem1  40317  3atlem2  40318  llni2  40346  llnle  40352  2at0mat0  40359  2atm  40361  islpln5  40369  lplni2  40371  lplnnle2at  40375  2atnelpln  40378  islpln2a  40382  llncvrlpln2  40391  2atmat  40395  2llnjaN  40400  islvol5  40413  lvoli2  40415  lvolnle3at  40416  3atnelvolN  40420  islvol2aN  40426  4atlem0a  40427  4atlem3  40430  4atlem3a  40431  4atlem3b  40432  4atlem4a  40433  4atlem4b  40434  4atlem4c  40435  4atlem4d  40436  4atlem9  40437  4atlem10a  40438  4atlem10  40440  4atlem11a  40441  4atlem11b  40442  4atlem11  40443  4atlem12a  40444  4atlem12b  40445  4atlem12  40446  4at  40447  4at2  40448  lplncvrlvol2  40449  2lplnja  40453  dalempjqeb  40479  dalemsjteb  40480  dalemtjueb  40481  dalemply  40488  dalem1  40493  dalemcea  40494  dalem3  40498  dalem4  40499  dalem5  40501  dalem-cly  40505  dalem17  40514  dalem21  40528  dalem24  40531  dalem25  40532  dalem27  40533  dalem38  40544  dalem39  40545  dalem43  40549  dalem44  40550  dalem45  40551  dalem55  40561  dalem56  40562  dalem57  40563  2atm2atN  40619  2llnma1b  40620  2llnma3r  40622  llnmod2i2  40697  llnexchb2lem  40702  dalawlem1  40705  dalawlem2  40706  dalawlem3  40707  dalawlem4  40708  dalawlem5  40709  dalawlem6  40710  dalawlem7  40711  dalawlem8  40712  dalawlem9  40713  dalawlem11  40715  dalawlem12  40716  dalawlem15  40719  lhp2lt  40835  lhpexle2lem  40843  lhpexle3lem  40845  lhp2at0  40866  lhp2atnle  40867  lhpat3  40880  4atexlempsb  40894  4atexlemqtb  40895  4atexlemunv  40900  4atexlemtlw  40901  4atexlemc  40903  4atexlemnclw  40904  4atexlemcnd  40906  trlval3  41021  trlval4  41022  cdlemc4  41028  cdlemc5  41029  cdlemc6  41030  cdlemd2  41033  cdleme0e  41051  cdlemeulpq  41054  cdleme01N  41055  cdleme0ex1N  41057  cdleme3g  41068  cdleme3h  41069  cdleme3  41071  cdleme4  41072  cdleme4a  41073  cdleme5  41074  cdleme7aa  41076  cdleme7c  41079  cdleme7d  41080  cdleme7e  41081  cdleme7ga  41082  cdleme7  41083  cdleme9b  41086  cdleme9  41087  cdleme10  41088  cdleme11c  41095  cdleme13  41106  cdleme15b  41109  cdleme15d  41111  cdleme15  41112  cdleme16b  41113  cdleme16e  41116  cdleme16f  41117  cdleme17b  41121  cdleme22gb  41128  cdlemedb  41131  cdlemednpq  41133  cdleme20zN  41135  cdleme19a  41137  cdleme19c  41139  cdleme20aN  41143  cdleme20c  41145  cdleme20d  41146  cdleme20e  41147  cdleme20j  41152  cdleme20l  41156  cdleme21c  41161  cdleme21ct  41163  cdleme22aa  41173  cdleme22b  41175  cdleme22cN  41176  cdleme22d  41177  cdleme22e  41178  cdleme22eALTN  41179  cdleme22f  41180  cdleme22g  41182  cdleme23a  41183  cdleme23b  41184  cdleme23c  41185  cdleme28a  41204  cdleme35a  41282  cdleme35fnpq  41283  cdleme35b  41284  cdleme35c  41285  cdleme35d  41286  cdleme35e  41287  cdleme35f  41288  cdleme42a  41305  cdleme42c  41306  cdleme42h  41316  cdleme42i  41317  cdlemeg46frv  41359  cdlemeg46vrg  41361  cdlemeg46rgv  41362  cdlemeg46req  41363  cdlemf1  41395  cdlemf2  41396  cdlemg2fv2  41434  cdlemg2m  41438  cdlemg4  41451  cdlemg8b  41462  cdlemg10bALTN  41470  cdlemg10c  41473  cdlemg10  41475  cdlemg12e  41481  cdlemg12f  41482  cdlemg12g  41483  cdlemg12  41484  cdlemg13a  41485  cdlemg17a  41495  cdlemg17dALTN  41498  cdlemg17h  41502  cdlemg17  41511  cdlemg18b  41513  cdlemg19a  41517  cdlemg19  41518  cdlemg27a  41526  cdlemg27b  41530  cdlemg31a  41531  cdlemg31b  41532  cdlemg33b0  41535  cdlemg33a  41540  trlcoabs2N  41556  trlcolem  41560  cdlemg42  41563  cdlemg46  41569  cdlemh1  41649  cdlemk3  41667  cdlemk10  41677  cdlemk12  41684  cdlemkole  41687  cdlemk14  41688  cdlemk15  41689  cdlemk1u  41693  cdlemk5u  41695  cdlemk12u  41706  cdlemk37  41748  cdlemk39  41750  cdlemkid1  41756  cdlemk51  41787  cdlemk52  41788  dia2dimlem1  41898  dia2dimlem2  41899  dia2dimlem3  41900  dia2dimlem10  41907  dia2dimlem12  41909  cdlemm10N  41952  cdlemn2  42029  cdlemn10  42040  dib2dim  42077  dih2dimb  42078  dih2dimbALTN  42079  dihjatcclem1  42252  dihjatcclem2  42253  dihjatcclem4  42255  dvh4dimat  42272