Theorem hlatjcl 40690

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ‘cfv 6566  (class class class)co 7451  Basecbs 17431  joincjn 18535  Latclat 18655  Atomscatm 40586  HLchlt 40673

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-lub 18568  df-glb 18569  df-join 18570  df-meet 18571  df-lat 18656  df-ats 40590  df-atl 40621  df-cvlat 40645  df-hlat 40674

This theorem is used by:  atcvr0eq  40749  2atjm  40768  atbtwn  40769  3dim0  40780  3dimlem3a  40783  3dimlem3OLDN  40785  3dimlem4OLDN  40788  3dim3  40792  2dim  40793  ps-1  40800  hlatexch3N  40803  hlatexch4  40804  ps-2b  40805  3atlem1  40806  3atlem2  40807  llni2  40835  llnle  40841  2at0mat0  40848  2atm  40850  islpln5  40858  lplni2  40860  lplnnle2at  40864  2atnelpln  40867  islpln2a  40871  llncvrlpln2  40880  2atmat  40884  2llnjaN  40889  islvol5  40902  lvoli2  40904  lvolnle3at  40905  3atnelvolN  40909  islvol2aN  40915  4atlem0a  40916  4atlem3  40919  4atlem3a  40920  4atlem3b  40921  4atlem4a  40922  4atlem4b  40923  4atlem4c  40924  4atlem4d  40925  4atlem9  40926  4atlem10a  40927  4atlem10  40929  4atlem11a  40930  4atlem11b  40931  4atlem11  40932  4atlem12a  40933  4atlem12b  40934  4atlem12  40935  4at  40936  4at2  40937  lplncvrlvol2  40938  2lplnja  40942  dalempjqeb  40968  dalemsjteb  40969  dalemtjueb  40970  dalemply  40977  dalem1  40982  dalemcea  40983  dalem3  40987  dalem4  40988  dalem5  40990  dalem-cly  40994  dalem17  41003  dalem21  41017  dalem24  41020  dalem25  41021  dalem27  41022  dalem38  41033  dalem39  41034  dalem43  41038  dalem44  41039  dalem45  41040  dalem55  41050  dalem56  41051  dalem57  41052  2atm2atN  41108  2llnma1b  41109  2llnma3r  41111  llnmod2i2  41186  llnexchb2lem  41191  dalawlem1  41194  dalawlem2  41195  dalawlem3  41196  dalawlem4  41197  dalawlem5  41198  dalawlem6  41199  dalawlem7  41200  dalawlem8  41201  dalawlem9  41202  dalawlem11  41204  dalawlem12  41205  dalawlem15  41208  lhp2lt  41324  lhpexle2lem  41332  lhpexle3lem  41334  lhp2at0  41355  lhp2atnle  41356  lhpat3  41369  4atexlempsb  41383  4atexlemqtb  41384  4atexlemunv  41389  4atexlemtlw  41390  4atexlemc  41392  4atexlemnclw  41393  4atexlemcnd  41395  trlval3  41510  trlval4  41511  cdlemc4  41517  cdlemc5  41518  cdlemc6  41519  cdlemd2  41522  cdleme0e  41540  cdlemeulpq  41543  cdleme01N  41544  cdleme0ex1N  41546  cdleme3g  41557  cdleme3h  41558  cdleme3  41560  cdleme4  41561  cdleme4a  41562  cdleme5  41563  cdleme7aa  41565  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme7ga  41571  cdleme7  41572  cdleme9b  41575  cdleme9  41576  cdleme10  41577  cdleme11c  41584  cdleme13  41595  cdleme15b  41598  cdleme15d  41600  cdleme15  41601  cdleme16b  41602  cdleme16e  41605  cdleme16f  41606  cdleme17b  41610  cdleme22gb  41617  cdlemedb  41620  cdlemednpq  41622  cdleme20zN  41624  cdleme19a  41626  cdleme19c  41628  cdleme20aN  41632  cdleme20c  41634  cdleme20d  41635  cdleme20e  41636  cdleme20j  41641  cdleme20l  41645  cdleme21c  41650  cdleme21ct  41652  cdleme22aa  41662  cdleme22b  41664  cdleme22cN  41665  cdleme22d  41666  cdleme22e  41667  cdleme22eALTN  41668  cdleme22f  41669  cdleme22g  41671  cdleme23a  41672  cdleme23b  41673  cdleme23c  41674  cdleme28a  41693  cdleme35a  41771  cdleme35fnpq  41772  cdleme35b  41773  cdleme35c  41774  cdleme35d  41775  cdleme35e  41776  cdleme35f  41777  cdleme42a  41794  cdleme42c  41795  cdleme42h  41805  cdleme42i  41806  cdlemeg46frv  41848  cdlemeg46vrg  41850  cdlemeg46rgv  41851  cdlemeg46req  41852  cdlemf1  41884  cdlemf2  41885  cdlemg2fv2  41923  cdlemg2m  41927  cdlemg4  41940  cdlemg8b  41951  cdlemg10bALTN  41959  cdlemg10c  41962  cdlemg10  41964  cdlemg12e  41970  cdlemg12f  41971  cdlemg12g  41972  cdlemg12  41973  cdlemg13a  41974  cdlemg17a  41984  cdlemg17dALTN  41987  cdlemg17h  41991  cdlemg17  42000  cdlemg18b  42002  cdlemg19a  42006  cdlemg19  42007  cdlemg27a  42015  cdlemg27b  42019  cdlemg31a  42020  cdlemg31b  42021  cdlemg33b0  42024  cdlemg33a  42029  trlcoabs2N  42045  trlcolem  42049  cdlemg42  42052  cdlemg46  42058  cdlemh1  42138  cdlemk3  42156  cdlemk10  42166  cdlemk12  42173  cdlemkole  42176  cdlemk14  42177  cdlemk15  42178  cdlemk1u  42182  cdlemk5u  42184  cdlemk12u  42195  cdlemk37  42237  cdlemk39  42239  cdlemkid1  42245  cdlemk51  42276  cdlemk52  42277  dia2dimlem1  42387  dia2dimlem2  42388  dia2dimlem3  42389  dia2dimlem10  42396  dia2dimlem12  42398  cdlemm10N  42441  cdlemn2  42518  cdlemn10  42529  dib2dim  42566  dih2dimb  42567  dih2dimbALTN  42568  dihjatcclem1  42741  dihjatcclem2  42742  dihjatcclem4  42744  dvh4dimat  42761