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

Theorem hlatjcl 30178
Description: Closure of join operation. Frequently-used special case of latjcl 14172 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 30175 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 hlatjcl.b . . 3  |-  B  =  ( Base `  K
)
3 hlatjcl.a . . 3  |-  A  =  ( Atoms `  K )
42, 3atbase 30101 . 2  |-  ( X  e.  A  ->  X  e.  B )
52, 3atbase 30101 . 2  |-  ( Y  e.  A  ->  Y  e.  B )
6 hlatjcl.j . . 3  |-  .\/  =  ( join `  K )
72, 6latjcl 14172 . 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 1632    e. wcel 1696   ` cfv 5271  (class class class)co 5874   Basecbs 13164   joincjn 14094   Latclat 14167   Atomscatm 30075   HLchlt 30162
This theorem is referenced by:  atcvr0eq  30237  2atjm  30256  atbtwn  30257  3dim0  30268  3dimlem3a  30271  3dimlem3OLDN  30273  3dimlem4OLDN  30276  3dim3  30280  2dim  30281  ps-1  30288  hlatexch3N  30291  hlatexch4  30292  ps-2b  30293  3atlem1  30294  3atlem2  30295  llni2  30323  llnle  30329  2at0mat0  30336  2atm  30338  islpln5  30346  lplni2  30348  lplnnle2at  30352  2atnelpln  30355  islpln2a  30359  llncvrlpln2  30368  2atmat  30372  2llnjaN  30377  islvol5  30390  lvoli2  30392  lvolnle3at  30393  3atnelvolN  30397  islvol2aN  30403  4atlem0a  30404  4atlem3  30407  4atlem3a  30408  4atlem3b  30409  4atlem4a  30410  4atlem4b  30411  4atlem4c  30412  4atlem4d  30413  4atlem9  30414  4atlem10a  30415  4atlem10  30417  4atlem11a  30418  4atlem11b  30419  4atlem11  30420  4atlem12a  30421  4atlem12b  30422  4atlem12  30423  4at  30424  4at2  30425  lplncvrlvol2  30426  2lplnja  30430  dalempjqeb  30456  dalemsjteb  30457  dalemtjueb  30458  dalemply  30465  dalem1  30470  dalemcea  30471  dalem3  30475  dalem4  30476  dalem5  30478  dalem-cly  30482  dalem17  30491  dalem21  30505  dalem24  30508  dalem25  30509  dalem27  30510  dalem38  30521  dalem39  30522  dalem43  30526  dalem44  30527  dalem45  30528  dalem55  30538  dalem56  30539  dalem57  30540  2atm2atN  30596  2llnma1b  30597  2llnma3r  30599  llnmod2i2  30674  llnexchb2lem  30679  dalawlem1  30682  dalawlem2  30683  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem9  30690  dalawlem11  30692  dalawlem12  30693  dalawlem15  30696  lhp2lt  30812  lhpexle2lem  30820  lhpexle3lem  30822  lhp2at0  30843  lhp2atnle  30844  lhpat3  30857  4atexlempsb  30871  4atexlemqtb  30872  4atexlemunv  30877  4atexlemtlw  30878  4atexlemc  30880  4atexlemnclw  30881  4atexlemcnd  30883  trlval3  30998  trlval4  30999  cdlemc4  31005  cdlemc5  31006  cdlemc6  31007  cdlemd2  31010  cdleme0e  31028  cdlemeulpq  31031  cdleme01N  31032  cdleme0ex1N  31034  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme4  31049  cdleme4a  31050  cdleme5  31051  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme9b  31063  cdleme9  31064  cdleme10  31065  cdleme11c  31072  cdleme13  31083  cdleme15b  31086  cdleme15d  31088  cdleme15  31089  cdleme16b  31090  cdleme16e  31093  cdleme16f  31094  cdleme17b  31098  cdleme22gb  31105  cdlemedb  31108  cdlemednpq  31110  cdleme20zN  31112  cdleme20y  31113  cdleme19a  31114  cdleme19c  31116  cdleme20aN  31120  cdleme20c  31122  cdleme20d  31123  cdleme20e  31124  cdleme20j  31129  cdleme20l  31133  cdleme21c  31138  cdleme21ct  31140  cdleme22aa  31150  cdleme22b  31152  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme22g  31159  cdleme23a  31160  cdleme23b  31161  cdleme23c  31162  cdleme28a  31181  cdleme35a  31259  cdleme35fnpq  31260  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35e  31264  cdleme35f  31265  cdleme42a  31282  cdleme42c  31283  cdleme42h  31293  cdleme42i  31294  cdlemeg46frv  31336  cdlemeg46vrg  31338  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemf1  31372  cdlemf2  31373  cdlemg2fv2  31411  cdlemg2m  31415  cdlemg4  31428  cdlemg8b  31439  cdlemg10bALTN  31447  cdlemg10c  31450  cdlemg10  31452  cdlemg12e  31458  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg17a  31472  cdlemg17dALTN  31475  cdlemg17h  31479  cdlemg17  31488  cdlemg18b  31490  cdlemg19a  31494  cdlemg19  31495  cdlemg27a  31503  cdlemg27b  31507  cdlemg31a  31508  cdlemg31b  31509  cdlemg33b0  31512  cdlemg33a  31517  trlcoabs2N  31533  trlcolem  31537  cdlemg42  31540  cdlemg46  31546  cdlemh1  31626  cdlemk3  31644  cdlemk10  31654  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk1u  31670  cdlemk5u  31672  cdlemk12u  31683  cdlemk37  31725  cdlemk39  31727  cdlemkid1  31733  cdlemk51  31764  cdlemk52  31765  dia2dimlem1  31876  dia2dimlem2  31877  dia2dimlem3  31878  dia2dimlem10  31885  dia2dimlem12  31887  cdlemm10N  31930  cdlemn2  32007  cdlemn10  32018  dib2dim  32055  dih2dimb  32056  dih2dimbALTN  32057  dihjatcclem1  32230  dihjatcclem2  32231  dihjatcclem4  32233  dvh4dimat  32250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fv 5279  df-ov 5877  df-lat 14168  df-ats 30079  df-atl 30110  df-cvlat 30134  df-hlat 30163
  Copyright terms: Public domain W3C validator