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

Theorem hlatjcl 32848
Description: Closure of join operation. Frequently-used special case of latjcl 16282 for atoms. (Contributed by NM, 15-Jun-2012.)
Hypotheses
Ref Expression
hlatjcl.b  |-  B  =  ( Base `  K
)
hlatjcl.j  |-  .\/  =  ( join `  K )
hlatjcl.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
hlatjcl  |-  ( ( K  e.  HL  /\  X  e.  A  /\  Y  e.  A )  ->  ( X  .\/  Y
)  e.  B )

Proof of Theorem hlatjcl
StepHypRef Expression
1 hllat 32845 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 hlatjcl.b . . 3  |-  B  =  ( Base `  K
)
3 hlatjcl.a . . 3  |-  A  =  ( Atoms `  K )
42, 3atbase 32771 . 2  |-  ( X  e.  A  ->  X  e.  B )
52, 3atbase 32771 . 2  |-  ( Y  e.  A  ->  Y  e.  B )
6 hlatjcl.j . . 3  |-  .\/  =  ( join `  K )
72, 6latjcl 16282 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
81, 4, 5, 7syl3an 1306 1  |-  ( ( K  e.  HL  /\  X  e.  A  /\  Y  e.  A )  ->  ( X  .\/  Y
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982    = wceq 1437    e. wcel 1868   ` cfv 5597  (class class class)co 6301   Basecbs 15106   joincjn 16174   Latclat 16276   Atomscatm 32745   HLchlt 32832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-lub 16205  df-glb 16206  df-join 16207  df-meet 16208  df-lat 16277  df-ats 32749  df-atl 32780  df-cvlat 32804  df-hlat 32833
This theorem is referenced by:  atcvr0eq  32907  2atjm  32926  atbtwn  32927  3dim0  32938  3dimlem3a  32941  3dimlem3OLDN  32943  3dimlem4OLDN  32946  3dim3  32950  2dim  32951  ps-1  32958  hlatexch3N  32961  hlatexch4  32962  ps-2b  32963  3atlem1  32964  3atlem2  32965  llni2  32993  llnle  32999  2at0mat0  33006  2atm  33008  islpln5  33016  lplni2  33018  lplnnle2at  33022  2atnelpln  33025  islpln2a  33029  llncvrlpln2  33038  2atmat  33042  2llnjaN  33047  islvol5  33060  lvoli2  33062  lvolnle3at  33063  3atnelvolN  33067  islvol2aN  33073  4atlem0a  33074  4atlem3  33077  4atlem3a  33078  4atlem3b  33079  4atlem4a  33080  4atlem4b  33081  4atlem4c  33082  4atlem4d  33083  4atlem9  33084  4atlem10a  33085  4atlem10  33087  4atlem11a  33088  4atlem11b  33089  4atlem11  33090  4atlem12a  33091  4atlem12b  33092  4atlem12  33093  4at  33094  4at2  33095  lplncvrlvol2  33096  2lplnja  33100  dalempjqeb  33126  dalemsjteb  33127  dalemtjueb  33128  dalemply  33135  dalem1  33140  dalemcea  33141  dalem3  33145  dalem4  33146  dalem5  33148  dalem-cly  33152  dalem17  33161  dalem21  33175  dalem24  33178  dalem25  33179  dalem27  33180  dalem38  33191  dalem39  33192  dalem43  33196  dalem44  33197  dalem45  33198  dalem55  33208  dalem56  33209  dalem57  33210  2atm2atN  33266  2llnma1b  33267  2llnma3r  33269  llnmod2i2  33344  llnexchb2lem  33349  dalawlem1  33352  dalawlem2  33353  dalawlem3  33354  dalawlem4  33355  dalawlem5  33356  dalawlem6  33357  dalawlem7  33358  dalawlem8  33359  dalawlem9  33360  dalawlem11  33362  dalawlem12  33363  dalawlem15  33366  lhp2lt  33482  lhpexle2lem  33490  lhpexle3lem  33492  lhp2at0  33513  lhp2atnle  33514  lhpat3  33527  4atexlempsb  33541  4atexlemqtb  33542  4atexlemunv  33547  4atexlemtlw  33548  4atexlemc  33550  4atexlemnclw  33551  4atexlemcnd  33553  trlval3  33669  trlval4  33670  cdlemc4  33676  cdlemc5  33677  cdlemc6  33678  cdlemd2  33681  cdleme0e  33699  cdlemeulpq  33702  cdleme01N  33703  cdleme0ex1N  33705  cdleme3g  33716  cdleme3h  33717  cdleme3  33719  cdleme4  33720  cdleme4a  33721  cdleme5  33722  cdleme7aa  33724  cdleme7c  33727  cdleme7d  33728  cdleme7e  33729  cdleme7ga  33730  cdleme7  33731  cdleme9b  33734  cdleme9  33735  cdleme10  33736  cdleme11c  33743  cdleme13  33754  cdleme15b  33757  cdleme15d  33759  cdleme15  33760  cdleme16b  33761  cdleme16e  33764  cdleme16f  33765  cdleme17b  33769  cdleme22gb  33776  cdlemedb  33779  cdlemednpq  33781  cdleme20zN  33783  cdleme20yOLD  33785  cdleme19a  33786  cdleme19c  33788  cdleme20aN  33792  cdleme20c  33794  cdleme20d  33795  cdleme20e  33796  cdleme20j  33801  cdleme20l  33805  cdleme21c  33810  cdleme21ct  33812  cdleme22aa  33822  cdleme22b  33824  cdleme22cN  33825  cdleme22d  33826  cdleme22e  33827  cdleme22eALTN  33828  cdleme22f  33829  cdleme22g  33831  cdleme23a  33832  cdleme23b  33833  cdleme23c  33834  cdleme28a  33853  cdleme35a  33931  cdleme35fnpq  33932  cdleme35b  33933  cdleme35c  33934  cdleme35d  33935  cdleme35e  33936  cdleme35f  33937  cdleme42a  33954  cdleme42c  33955  cdleme42h  33965  cdleme42i  33966  cdlemeg46frv  34008  cdlemeg46vrg  34010  cdlemeg46rgv  34011  cdlemeg46req  34012  cdlemf1  34044  cdlemf2  34045  cdlemg2fv2  34083  cdlemg2m  34087  cdlemg4  34100  cdlemg8b  34111  cdlemg10bALTN  34119  cdlemg10c  34122  cdlemg10  34124  cdlemg12e  34130  cdlemg12f  34131  cdlemg12g  34132  cdlemg12  34133  cdlemg13a  34134  cdlemg17a  34144  cdlemg17dALTN  34147  cdlemg17h  34151  cdlemg17  34160  cdlemg18b  34162  cdlemg19a  34166  cdlemg19  34167  cdlemg27a  34175  cdlemg27b  34179  cdlemg31a  34180  cdlemg31b  34181  cdlemg33b0  34184  cdlemg33a  34189  trlcoabs2N  34205  trlcolem  34209  cdlemg42  34212  cdlemg46  34218  cdlemh1  34298  cdlemk3  34316  cdlemk10  34326  cdlemk12  34333  cdlemkole  34336  cdlemk14  34337  cdlemk15  34338  cdlemk1u  34342  cdlemk5u  34344  cdlemk12u  34355  cdlemk37  34397  cdlemk39  34399  cdlemkid1  34405  cdlemk51  34436  cdlemk52  34437  dia2dimlem1  34548  dia2dimlem2  34549  dia2dimlem3  34550  dia2dimlem10  34557  dia2dimlem12  34559  cdlemm10N  34602  cdlemn2  34679  cdlemn10  34690  dib2dim  34727  dih2dimb  34728  dih2dimbALTN  34729  dihjatcclem1  34902  dihjatcclem2  34903  dihjatcclem4  34905  dvh4dimat  34922
  Copyright terms: Public domain W3C validator