Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlatjcl Structured version   Visualization version   GIF version

Theorem hlatjcl 35156
Description: Closure of join operation. Frequently-used special case of latjcl 17252 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
StepHypRef Expression
1 hllat 35153 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐵 = (Base‘𝐾)
3 hlatjcl.a . . 3 𝐴 = (Atoms‘𝐾)
42, 3atbase 35079 . 2 (𝑋𝐴𝑋𝐵)
52, 3atbase 35079 . 2 (𝑌𝐴𝑌𝐵)
6 hlatjcl.j . . 3 = (join‘𝐾)
72, 6latjcl 17252 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
81, 4, 5, 7syl3an 1164 1 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1632  wcel 2139  cfv 6049  (class class class)co 6813  Basecbs 16059  joincjn 17145  Latclat 17246  Atomscatm 35053  HLchlt 35140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-lub 17175  df-glb 17176  df-join 17177  df-meet 17178  df-lat 17247  df-ats 35057  df-atl 35088  df-cvlat 35112  df-hlat 35141
This theorem is referenced by:  atcvr0eq  35215  2atjm  35234  atbtwn  35235  3dim0  35246  3dimlem3a  35249  3dimlem3OLDN  35251  3dimlem4OLDN  35254  3dim3  35258  2dim  35259  ps-1  35266  hlatexch3N  35269  hlatexch4  35270  ps-2b  35271  3atlem1  35272  3atlem2  35273  llni2  35301  llnle  35307  2at0mat0  35314  2atm  35316  islpln5  35324  lplni2  35326  lplnnle2at  35330  2atnelpln  35333  islpln2a  35337  llncvrlpln2  35346  2atmat  35350  2llnjaN  35355  islvol5  35368  lvoli2  35370  lvolnle3at  35371  3atnelvolN  35375  islvol2aN  35381  4atlem0a  35382  4atlem3  35385  4atlem3a  35386  4atlem3b  35387  4atlem4a  35388  4atlem4b  35389  4atlem4c  35390  4atlem4d  35391  4atlem9  35392  4atlem10a  35393  4atlem10  35395  4atlem11a  35396  4atlem11b  35397  4atlem11  35398  4atlem12a  35399  4atlem12b  35400  4atlem12  35401  4at  35402  4at2  35403  lplncvrlvol2  35404  2lplnja  35408  dalempjqeb  35434  dalemsjteb  35435  dalemtjueb  35436  dalemply  35443  dalem1  35448  dalemcea  35449  dalem3  35453  dalem4  35454  dalem5  35456  dalem-cly  35460  dalem17  35469  dalem21  35483  dalem24  35486  dalem25  35487  dalem27  35488  dalem38  35499  dalem39  35500  dalem43  35504  dalem44  35505  dalem45  35506  dalem55  35516  dalem56  35517  dalem57  35518  2atm2atN  35574  2llnma1b  35575  2llnma3r  35577  llnmod2i2  35652  llnexchb2lem  35657  dalawlem1  35660  dalawlem2  35661  dalawlem3  35662  dalawlem4  35663  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem9  35668  dalawlem11  35670  dalawlem12  35671  dalawlem15  35674  lhp2lt  35790  lhpexle2lem  35798  lhpexle3lem  35800  lhp2at0  35821  lhp2atnle  35822  lhpat3  35835  4atexlempsb  35849  4atexlemqtb  35850  4atexlemunv  35855  4atexlemtlw  35856  4atexlemc  35858  4atexlemnclw  35859  4atexlemcnd  35861  trlval3  35977  trlval4  35978  cdlemc4  35984  cdlemc5  35985  cdlemc6  35986  cdlemd2  35989  cdleme0e  36007  cdlemeulpq  36010  cdleme01N  36011  cdleme0ex1N  36013  cdleme3g  36024  cdleme3h  36025  cdleme3  36027  cdleme4  36028  cdleme4a  36029  cdleme5  36030  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme9b  36042  cdleme9  36043  cdleme10  36044  cdleme11c  36051  cdleme13  36062  cdleme15b  36065  cdleme15d  36067  cdleme15  36068  cdleme16b  36069  cdleme16e  36072  cdleme16f  36073  cdleme17b  36077  cdleme22gb  36084  cdlemedb  36087  cdlemednpq  36089  cdleme20zN  36091  cdleme19a  36093  cdleme19c  36095  cdleme20aN  36099  cdleme20c  36101  cdleme20d  36102  cdleme20e  36103  cdleme20j  36108  cdleme20l  36112  cdleme21c  36117  cdleme21ct  36119  cdleme22aa  36129  cdleme22b  36131  cdleme22cN  36132  cdleme22d  36133  cdleme22e  36134  cdleme22eALTN  36135  cdleme22f  36136  cdleme22g  36138  cdleme23a  36139  cdleme23b  36140  cdleme23c  36141  cdleme28a  36160  cdleme35a  36238  cdleme35fnpq  36239  cdleme35b  36240  cdleme35c  36241  cdleme35d  36242  cdleme35e  36243  cdleme35f  36244  cdleme42a  36261  cdleme42c  36262  cdleme42h  36272  cdleme42i  36273  cdlemeg46frv  36315  cdlemeg46vrg  36317  cdlemeg46rgv  36318  cdlemeg46req  36319  cdlemf1  36351  cdlemf2  36352  cdlemg2fv2  36390  cdlemg2m  36394  cdlemg4  36407  cdlemg8b  36418  cdlemg10bALTN  36426  cdlemg10c  36429  cdlemg10  36431  cdlemg12e  36437  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg17a  36451  cdlemg17dALTN  36454  cdlemg17h  36458  cdlemg17  36467  cdlemg18b  36469  cdlemg19a  36473  cdlemg19  36474  cdlemg27a  36482  cdlemg27b  36486  cdlemg31a  36487  cdlemg31b  36488  cdlemg33b0  36491  cdlemg33a  36496  trlcoabs2N  36512  trlcolem  36516  cdlemg42  36519  cdlemg46  36525  cdlemh1  36605  cdlemk3  36623  cdlemk10  36633  cdlemk12  36640  cdlemkole  36643  cdlemk14  36644  cdlemk15  36645  cdlemk1u  36649  cdlemk5u  36651  cdlemk12u  36662  cdlemk37  36704  cdlemk39  36706  cdlemkid1  36712  cdlemk51  36743  cdlemk52  36744  dia2dimlem1  36855  dia2dimlem2  36856  dia2dimlem3  36857  dia2dimlem10  36864  dia2dimlem12  36866  cdlemm10N  36909  cdlemn2  36986  cdlemn10  36997  dib2dim  37034  dih2dimb  37035  dih2dimbALTN  37036  dihjatcclem1  37209  dihjatcclem2  37210  dihjatcclem4  37212  dvh4dimat  37229
  Copyright terms: Public domain W3C validator