Theorem hlatjcl 39348

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  joincjn 18368  Latclat 18488  Atomscatm 39244  HLchlt 39331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-lub 18403  df-glb 18404  df-join 18405  df-meet 18406  df-lat 18489  df-ats 39248  df-atl 39279  df-cvlat 39303  df-hlat 39332

This theorem is referenced by:  atcvr0eq  39408  2atjm  39427  atbtwn  39428  3dim0  39439  3dimlem3a  39442  3dimlem3OLDN  39444  3dimlem4OLDN  39447  3dim3  39451  2dim  39452  ps-1  39459  hlatexch3N  39462  hlatexch4  39463  ps-2b  39464  3atlem1  39465  3atlem2  39466  llni2  39494  llnle  39500  2at0mat0  39507  2atm  39509  islpln5  39517  lplni2  39519  lplnnle2at  39523  2atnelpln  39526  islpln2a  39530  llncvrlpln2  39539  2atmat  39543  2llnjaN  39548  islvol5  39561  lvoli2  39563  lvolnle3at  39564  3atnelvolN  39568  islvol2aN  39574  4atlem0a  39575  4atlem3  39578  4atlem3a  39579  4atlem3b  39580  4atlem4a  39581  4atlem4b  39582  4atlem4c  39583  4atlem4d  39584  4atlem9  39585  4atlem10a  39586  4atlem10  39588  4atlem11a  39589  4atlem11b  39590  4atlem11  39591  4atlem12a  39592  4atlem12b  39593  4atlem12  39594  4at  39595  4at2  39596  lplncvrlvol2  39597  2lplnja  39601  dalempjqeb  39627  dalemsjteb  39628  dalemtjueb  39629  dalemply  39636  dalem1  39641  dalemcea  39642  dalem3  39646  dalem4  39647  dalem5  39649  dalem-cly  39653  dalem17  39662  dalem21  39676  dalem24  39679  dalem25  39680  dalem27  39681  dalem38  39692  dalem39  39693  dalem43  39697  dalem44  39698  dalem45  39699  dalem55  39709  dalem56  39710  dalem57  39711  2atm2atN  39767  2llnma1b  39768  2llnma3r  39770  llnmod2i2  39845  llnexchb2lem  39850  dalawlem1  39853  dalawlem2  39854  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem11  39863  dalawlem12  39864  dalawlem15  39867  lhp2lt  39983  lhpexle2lem  39991  lhpexle3lem  39993  lhp2at0  40014  lhp2atnle  40015  lhpat3  40028  4atexlempsb  40042  4atexlemqtb  40043  4atexlemunv  40048  4atexlemtlw  40049  4atexlemc  40051  4atexlemnclw  40052  4atexlemcnd  40054  trlval3  40169  trlval4  40170  cdlemc4  40176  cdlemc5  40177  cdlemc6  40178  cdlemd2  40181  cdleme0e  40199  cdlemeulpq  40202  cdleme01N  40203  cdleme0ex1N  40205  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme4  40220  cdleme4a  40221  cdleme5  40222  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme9b  40234  cdleme9  40235  cdleme10  40236  cdleme11c  40243  cdleme13  40254  cdleme15b  40257  cdleme15d  40259  cdleme15  40260  cdleme16b  40261  cdleme16e  40264  cdleme16f  40265  cdleme17b  40269  cdleme22gb  40276  cdlemedb  40279  cdlemednpq  40281  cdleme20zN  40283  cdleme19a  40285  cdleme19c  40287  cdleme20aN  40291  cdleme20c  40293  cdleme20d  40294  cdleme20e  40295  cdleme20j  40300  cdleme20l  40304  cdleme21c  40309  cdleme21ct  40311  cdleme22aa  40321  cdleme22b  40323  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme22g  40330  cdleme23a  40331  cdleme23b  40332  cdleme23c  40333  cdleme28a  40352  cdleme35a  40430  cdleme35fnpq  40431  cdleme35b  40432  cdleme35c  40433  cdleme35d  40434  cdleme35e  40435  cdleme35f  40436  cdleme42a  40453  cdleme42c  40454  cdleme42h  40464  cdleme42i  40465  cdlemeg46frv  40507  cdlemeg46vrg  40509  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemf1  40543  cdlemf2  40544  cdlemg2fv2  40582  cdlemg2m  40586  cdlemg4  40599  cdlemg8b  40610  cdlemg10bALTN  40618  cdlemg10c  40621  cdlemg10  40623  cdlemg12e  40629  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg17a  40643  cdlemg17dALTN  40646  cdlemg17h  40650  cdlemg17  40659  cdlemg18b  40661  cdlemg19a  40665  cdlemg19  40666  cdlemg27a  40674  cdlemg27b  40678  cdlemg31a  40679  cdlemg31b  40680  cdlemg33b0  40683  cdlemg33a  40688  trlcoabs2N  40704  trlcolem  40708  cdlemg42  40711  cdlemg46  40717  cdlemh1  40797  cdlemk3  40815  cdlemk10  40825  cdlemk12  40832  cdlemkole  40835  cdlemk14  40836  cdlemk15  40837  cdlemk1u  40841  cdlemk5u  40843  cdlemk12u  40854  cdlemk37  40896  cdlemk39  40898  cdlemkid1  40904  cdlemk51  40935  cdlemk52  40936  dia2dimlem1  41046  dia2dimlem2  41047  dia2dimlem3  41048  dia2dimlem10  41055  dia2dimlem12  41057  cdlemm10N  41100  cdlemn2  41177  cdlemn10  41188  dib2dim  41225  dih2dimb  41226  dih2dimbALTN  41227  dihjatcclem1  41400  dihjatcclem2  41401  dihjatcclem4  41403  dvh4dimat  41420