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 34133
Description: Closure of join operation. Frequently-used special case of latjcl 16972 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 34130 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐵 = (Base‘𝐾)
3 hlatjcl.a . . 3 𝐴 = (Atoms‘𝐾)
42, 3atbase 34056 . 2 (𝑋𝐴𝑋𝐵)
52, 3atbase 34056 . 2 (𝑌𝐴𝑌𝐵)
6 hlatjcl.j . . 3 = (join‘𝐾)
72, 6latjcl 16972 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
81, 4, 5, 7syl3an 1365 1 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1480  wcel 1987  cfv 5847  (class class class)co 6604  Basecbs 15781  joincjn 16865  Latclat 16966  Atomscatm 34030  HLchlt 34117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-lub 16895  df-glb 16896  df-join 16897  df-meet 16898  df-lat 16967  df-ats 34034  df-atl 34065  df-cvlat 34089  df-hlat 34118
This theorem is referenced by:  atcvr0eq  34192  2atjm  34211  atbtwn  34212  3dim0  34223  3dimlem3a  34226  3dimlem3OLDN  34228  3dimlem4OLDN  34231  3dim3  34235  2dim  34236  ps-1  34243  hlatexch3N  34246  hlatexch4  34247  ps-2b  34248  3atlem1  34249  3atlem2  34250  llni2  34278  llnle  34284  2at0mat0  34291  2atm  34293  islpln5  34301  lplni2  34303  lplnnle2at  34307  2atnelpln  34310  islpln2a  34314  llncvrlpln2  34323  2atmat  34327  2llnjaN  34332  islvol5  34345  lvoli2  34347  lvolnle3at  34348  3atnelvolN  34352  islvol2aN  34358  4atlem0a  34359  4atlem3  34362  4atlem3a  34363  4atlem3b  34364  4atlem4a  34365  4atlem4b  34366  4atlem4c  34367  4atlem4d  34368  4atlem9  34369  4atlem10a  34370  4atlem10  34372  4atlem11a  34373  4atlem11b  34374  4atlem11  34375  4atlem12a  34376  4atlem12b  34377  4atlem12  34378  4at  34379  4at2  34380  lplncvrlvol2  34381  2lplnja  34385  dalempjqeb  34411  dalemsjteb  34412  dalemtjueb  34413  dalemply  34420  dalem1  34425  dalemcea  34426  dalem3  34430  dalem4  34431  dalem5  34433  dalem-cly  34437  dalem17  34446  dalem21  34460  dalem24  34463  dalem25  34464  dalem27  34465  dalem38  34476  dalem39  34477  dalem43  34481  dalem44  34482  dalem45  34483  dalem55  34493  dalem56  34494  dalem57  34495  2atm2atN  34551  2llnma1b  34552  2llnma3r  34554  llnmod2i2  34629  llnexchb2lem  34634  dalawlem1  34637  dalawlem2  34638  dalawlem3  34639  dalawlem4  34640  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem9  34645  dalawlem11  34647  dalawlem12  34648  dalawlem15  34651  lhp2lt  34767  lhpexle2lem  34775  lhpexle3lem  34777  lhp2at0  34798  lhp2atnle  34799  lhpat3  34812  4atexlempsb  34826  4atexlemqtb  34827  4atexlemunv  34832  4atexlemtlw  34833  4atexlemc  34835  4atexlemnclw  34836  4atexlemcnd  34838  trlval3  34954  trlval4  34955  cdlemc4  34961  cdlemc5  34962  cdlemc6  34963  cdlemd2  34966  cdleme0e  34984  cdlemeulpq  34987  cdleme01N  34988  cdleme0ex1N  34990  cdleme3g  35001  cdleme3h  35002  cdleme3  35004  cdleme4  35005  cdleme4a  35006  cdleme5  35007  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme7  35016  cdleme9b  35019  cdleme9  35020  cdleme10  35021  cdleme11c  35028  cdleme13  35039  cdleme15b  35042  cdleme15d  35044  cdleme15  35045  cdleme16b  35046  cdleme16e  35049  cdleme16f  35050  cdleme17b  35054  cdleme22gb  35061  cdlemedb  35064  cdlemednpq  35066  cdleme20zN  35068  cdleme20yOLD  35070  cdleme19a  35071  cdleme19c  35073  cdleme20aN  35077  cdleme20c  35079  cdleme20d  35080  cdleme20e  35081  cdleme20j  35086  cdleme20l  35090  cdleme21c  35095  cdleme21ct  35097  cdleme22aa  35107  cdleme22b  35109  cdleme22cN  35110  cdleme22d  35111  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f  35114  cdleme22g  35116  cdleme23a  35117  cdleme23b  35118  cdleme23c  35119  cdleme28a  35138  cdleme35a  35216  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme35e  35221  cdleme35f  35222  cdleme42a  35239  cdleme42c  35240  cdleme42h  35250  cdleme42i  35251  cdlemeg46frv  35293  cdlemeg46vrg  35295  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemf1  35329  cdlemf2  35330  cdlemg2fv2  35368  cdlemg2m  35372  cdlemg4  35385  cdlemg8b  35396  cdlemg10bALTN  35404  cdlemg10c  35407  cdlemg10  35409  cdlemg12e  35415  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg17a  35429  cdlemg17dALTN  35432  cdlemg17h  35436  cdlemg17  35445  cdlemg18b  35447  cdlemg19a  35451  cdlemg19  35452  cdlemg27a  35460  cdlemg27b  35464  cdlemg31a  35465  cdlemg31b  35466  cdlemg33b0  35469  cdlemg33a  35474  trlcoabs2N  35490  trlcolem  35494  cdlemg42  35497  cdlemg46  35503  cdlemh1  35583  cdlemk3  35601  cdlemk10  35611  cdlemk12  35618  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk1u  35627  cdlemk5u  35629  cdlemk12u  35640  cdlemk37  35682  cdlemk39  35684  cdlemkid1  35690  cdlemk51  35721  cdlemk52  35722  dia2dimlem1  35833  dia2dimlem2  35834  dia2dimlem3  35835  dia2dimlem10  35842  dia2dimlem12  35844  cdlemm10N  35887  cdlemn2  35964  cdlemn10  35975  dib2dim  36012  dih2dimb  36013  dih2dimbALTN  36014  dihjatcclem1  36187  dihjatcclem2  36188  dihjatcclem4  36190  dvh4dimat  36207
  Copyright terms: Public domain W3C validator