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

Theorem hlatjcl 28929
Description: Closure of join operation. Frequently-used special case of latjcl 14156 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 28926 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 hlatjcl.b . . 3  |-  B  =  ( Base `  K
)
3 hlatjcl.a . . 3  |-  A  =  ( Atoms `  K )
42, 3atbase 28852 . 2  |-  ( X  e.  A  ->  X  e.  B )
52, 3atbase 28852 . 2  |-  ( Y  e.  A  ->  Y  e.  B )
6 hlatjcl.j . . 3  |-  .\/  =  ( join `  K )
72, 6latjcl 14156 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
81, 4, 5, 7syl3an 1224 1  |-  ( ( K  e.  HL  /\  X  e.  A  /\  Y  e.  A )  ->  ( X  .\/  Y
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    = wceq 1623    e. wcel 1684   ` cfv 5255  (class class class)co 5858   Basecbs 13148   joincjn 14078   Latclat 14151   Atomscatm 28826   HLchlt 28913
This theorem is referenced by:  atcvr0eq  28988  2atjm  29007  atbtwn  29008  3dim0  29019  3dimlem3a  29022  3dimlem3OLDN  29024  3dimlem4OLDN  29027  3dim3  29031  2dim  29032  ps-1  29039  hlatexch3N  29042  hlatexch4  29043  ps-2b  29044  3atlem1  29045  3atlem2  29046  llni2  29074  llnle  29080  2at0mat0  29087  2atm  29089  islpln5  29097  lplni2  29099  lplnnle2at  29103  2atnelpln  29106  islpln2a  29110  llncvrlpln2  29119  2atmat  29123  2llnjaN  29128  islvol5  29141  lvoli2  29143  lvolnle3at  29144  3atnelvolN  29148  islvol2aN  29154  4atlem0a  29155  4atlem3  29158  4atlem3a  29159  4atlem3b  29160  4atlem4a  29161  4atlem4b  29162  4atlem4c  29163  4atlem4d  29164  4atlem9  29165  4atlem10a  29166  4atlem10  29168  4atlem11a  29169  4atlem11b  29170  4atlem11  29171  4atlem12a  29172  4atlem12b  29173  4atlem12  29174  4at  29175  4at2  29176  lplncvrlvol2  29177  2lplnja  29181  dalempjqeb  29207  dalemsjteb  29208  dalemtjueb  29209  dalemply  29216  dalem1  29221  dalemcea  29222  dalem3  29226  dalem4  29227  dalem5  29229  dalem-cly  29233  dalem17  29242  dalem21  29256  dalem24  29259  dalem25  29260  dalem27  29261  dalem38  29272  dalem39  29273  dalem43  29277  dalem44  29278  dalem45  29279  dalem55  29289  dalem56  29290  dalem57  29291  2atm2atN  29347  2llnma1b  29348  2llnma3r  29350  llnmod2i2  29425  llnexchb2lem  29430  dalawlem1  29433  dalawlem2  29434  dalawlem3  29435  dalawlem4  29436  dalawlem5  29437  dalawlem6  29438  dalawlem7  29439  dalawlem8  29440  dalawlem9  29441  dalawlem11  29443  dalawlem12  29444  dalawlem15  29447  lhp2lt  29563  lhpexle2lem  29571  lhpexle3lem  29573  lhp2at0  29594  lhp2atnle  29595  lhpat3  29608  4atexlempsb  29622  4atexlemqtb  29623  4atexlemunv  29628  4atexlemtlw  29629  4atexlemc  29631  4atexlemnclw  29632  4atexlemcnd  29634  trlval3  29749  trlval4  29750  cdlemc4  29756  cdlemc5  29757  cdlemc6  29758  cdlemd2  29761  cdleme0e  29779  cdlemeulpq  29782  cdleme01N  29783  cdleme0ex1N  29785  cdleme3g  29796  cdleme3h  29797  cdleme3  29799  cdleme4  29800  cdleme4a  29801  cdleme5  29802  cdleme7aa  29804  cdleme7c  29807  cdleme7d  29808  cdleme7e  29809  cdleme7ga  29810  cdleme7  29811  cdleme9b  29814  cdleme9  29815  cdleme10  29816  cdleme11c  29823  cdleme13  29834  cdleme15b  29837  cdleme15d  29839  cdleme15  29840  cdleme16b  29841  cdleme16e  29844  cdleme16f  29845  cdleme17b  29849  cdleme22gb  29856  cdlemedb  29859  cdlemednpq  29861  cdleme20zN  29863  cdleme20y  29864  cdleme19a  29865  cdleme19c  29867  cdleme20aN  29871  cdleme20c  29873  cdleme20d  29874  cdleme20e  29875  cdleme20j  29880  cdleme20l  29884  cdleme21c  29889  cdleme21ct  29891  cdleme22aa  29901  cdleme22b  29903  cdleme22cN  29904  cdleme22d  29905  cdleme22e  29906  cdleme22eALTN  29907  cdleme22f  29908  cdleme22g  29910  cdleme23a  29911  cdleme23b  29912  cdleme23c  29913  cdleme28a  29932  cdleme35a  30010  cdleme35fnpq  30011  cdleme35b  30012  cdleme35c  30013  cdleme35d  30014  cdleme35e  30015  cdleme35f  30016  cdleme42a  30033  cdleme42c  30034  cdleme42h  30044  cdleme42i  30045  cdlemeg46frv  30087  cdlemeg46vrg  30089  cdlemeg46rgv  30090  cdlemeg46req  30091  cdlemf1  30123  cdlemf2  30124  cdlemg2fv2  30162  cdlemg2m  30166  cdlemg4  30179  cdlemg8b  30190  cdlemg10bALTN  30198  cdlemg10c  30201  cdlemg10  30203  cdlemg12e  30209  cdlemg12f  30210  cdlemg12g  30211  cdlemg12  30212  cdlemg13a  30213  cdlemg17a  30223  cdlemg17dALTN  30226  cdlemg17h  30230  cdlemg17  30239  cdlemg18b  30241  cdlemg19a  30245  cdlemg19  30246  cdlemg27a  30254  cdlemg27b  30258  cdlemg31a  30259  cdlemg31b  30260  cdlemg33b0  30263  cdlemg33a  30268  trlcoabs2N  30284  trlcolem  30288  cdlemg42  30291  cdlemg46  30297  cdlemh1  30377  cdlemk3  30395  cdlemk10  30405  cdlemk12  30412  cdlemkole  30415  cdlemk14  30416  cdlemk15  30417  cdlemk1u  30421  cdlemk5u  30423  cdlemk12u  30434  cdlemk37  30476  cdlemk39  30478  cdlemkid1  30484  cdlemk51  30515  cdlemk52  30516  dia2dimlem1  30627  dia2dimlem2  30628  dia2dimlem3  30629  dia2dimlem10  30636  dia2dimlem12  30638  cdlemm10N  30681  cdlemn2  30758  cdlemn10  30769  dib2dim  30806  dih2dimb  30807  dih2dimbALTN  30808  dihjatcclem1  30981  dihjatcclem2  30982  dihjatcclem4  30984  dvh4dimat  31001
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-ov 5861  df-lat 14152  df-ats 28830  df-atl 28861  df-cvlat 28885  df-hlat 28914
  Copyright terms: Public domain W3C validator