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

Theorem hlatjcl 30262
Description: Closure of join operation. Frequently-used special case of latjcl 14510 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 30259 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 hlatjcl.b . . 3  |-  B  =  ( Base `  K
)
3 hlatjcl.a . . 3  |-  A  =  ( Atoms `  K )
42, 3atbase 30185 . 2  |-  ( X  e.  A  ->  X  e.  B )
52, 3atbase 30185 . 2  |-  ( Y  e.  A  ->  Y  e.  B )
6 hlatjcl.j . . 3  |-  .\/  =  ( join `  K )
72, 6latjcl 14510 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
81, 4, 5, 7syl3an 1227 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 937    = wceq 1653    e. wcel 1727   ` cfv 5483  (class class class)co 6110   Basecbs 13500   joincjn 14432   Latclat 14505   Atomscatm 30159   HLchlt 30246
This theorem is referenced by:  atcvr0eq  30321  2atjm  30340  atbtwn  30341  3dim0  30352  3dimlem3a  30355  3dimlem3OLDN  30357  3dimlem4OLDN  30360  3dim3  30364  2dim  30365  ps-1  30372  hlatexch3N  30375  hlatexch4  30376  ps-2b  30377  3atlem1  30378  3atlem2  30379  llni2  30407  llnle  30413  2at0mat0  30420  2atm  30422  islpln5  30430  lplni2  30432  lplnnle2at  30436  2atnelpln  30439  islpln2a  30443  llncvrlpln2  30452  2atmat  30456  2llnjaN  30461  islvol5  30474  lvoli2  30476  lvolnle3at  30477  3atnelvolN  30481  islvol2aN  30487  4atlem0a  30488  4atlem3  30491  4atlem3a  30492  4atlem3b  30493  4atlem4a  30494  4atlem4b  30495  4atlem4c  30496  4atlem4d  30497  4atlem9  30498  4atlem10a  30499  4atlem10  30501  4atlem11a  30502  4atlem11b  30503  4atlem11  30504  4atlem12a  30505  4atlem12b  30506  4atlem12  30507  4at  30508  4at2  30509  lplncvrlvol2  30510  2lplnja  30514  dalempjqeb  30540  dalemsjteb  30541  dalemtjueb  30542  dalemply  30549  dalem1  30554  dalemcea  30555  dalem3  30559  dalem4  30560  dalem5  30562  dalem-cly  30566  dalem17  30575  dalem21  30589  dalem24  30592  dalem25  30593  dalem27  30594  dalem38  30605  dalem39  30606  dalem43  30610  dalem44  30611  dalem45  30612  dalem55  30622  dalem56  30623  dalem57  30624  2atm2atN  30680  2llnma1b  30681  2llnma3r  30683  llnmod2i2  30758  llnexchb2lem  30763  dalawlem1  30766  dalawlem2  30767  dalawlem3  30768  dalawlem4  30769  dalawlem5  30770  dalawlem6  30771  dalawlem7  30772  dalawlem8  30773  dalawlem9  30774  dalawlem11  30776  dalawlem12  30777  dalawlem15  30780  lhp2lt  30896  lhpexle2lem  30904  lhpexle3lem  30906  lhp2at0  30927  lhp2atnle  30928  lhpat3  30941  4atexlempsb  30955  4atexlemqtb  30956  4atexlemunv  30961  4atexlemtlw  30962  4atexlemc  30964  4atexlemnclw  30965  4atexlemcnd  30967  trlval3  31082  trlval4  31083  cdlemc4  31089  cdlemc5  31090  cdlemc6  31091  cdlemd2  31094  cdleme0e  31112  cdlemeulpq  31115  cdleme01N  31116  cdleme0ex1N  31118  cdleme3g  31129  cdleme3h  31130  cdleme3  31132  cdleme4  31133  cdleme4a  31134  cdleme5  31135  cdleme7aa  31137  cdleme7c  31140  cdleme7d  31141  cdleme7e  31142  cdleme7ga  31143  cdleme7  31144  cdleme9b  31147  cdleme9  31148  cdleme10  31149  cdleme11c  31156  cdleme13  31167  cdleme15b  31170  cdleme15d  31172  cdleme15  31173  cdleme16b  31174  cdleme16e  31177  cdleme16f  31178  cdleme17b  31182  cdleme22gb  31189  cdlemedb  31192  cdlemednpq  31194  cdleme20zN  31196  cdleme20y  31197  cdleme19a  31198  cdleme19c  31200  cdleme20aN  31204  cdleme20c  31206  cdleme20d  31207  cdleme20e  31208  cdleme20j  31213  cdleme20l  31217  cdleme21c  31222  cdleme21ct  31224  cdleme22aa  31234  cdleme22b  31236  cdleme22cN  31237  cdleme22d  31238  cdleme22e  31239  cdleme22eALTN  31240  cdleme22f  31241  cdleme22g  31243  cdleme23a  31244  cdleme23b  31245  cdleme23c  31246  cdleme28a  31265  cdleme35a  31343  cdleme35fnpq  31344  cdleme35b  31345  cdleme35c  31346  cdleme35d  31347  cdleme35e  31348  cdleme35f  31349  cdleme42a  31366  cdleme42c  31367  cdleme42h  31377  cdleme42i  31378  cdlemeg46frv  31420  cdlemeg46vrg  31422  cdlemeg46rgv  31423  cdlemeg46req  31424  cdlemf1  31456  cdlemf2  31457  cdlemg2fv2  31495  cdlemg2m  31499  cdlemg4  31512  cdlemg8b  31523  cdlemg10bALTN  31531  cdlemg10c  31534  cdlemg10  31536  cdlemg12e  31542  cdlemg12f  31543  cdlemg12g  31544  cdlemg12  31545  cdlemg13a  31546  cdlemg17a  31556  cdlemg17dALTN  31559  cdlemg17h  31563  cdlemg17  31572  cdlemg18b  31574  cdlemg19a  31578  cdlemg19  31579  cdlemg27a  31587  cdlemg27b  31591  cdlemg31a  31592  cdlemg31b  31593  cdlemg33b0  31596  cdlemg33a  31601  trlcoabs2N  31617  trlcolem  31621  cdlemg42  31624  cdlemg46  31630  cdlemh1  31710  cdlemk3  31728  cdlemk10  31738  cdlemk12  31745  cdlemkole  31748  cdlemk14  31749  cdlemk15  31750  cdlemk1u  31754  cdlemk5u  31756  cdlemk12u  31767  cdlemk37  31809  cdlemk39  31811  cdlemkid1  31817  cdlemk51  31848  cdlemk52  31849  dia2dimlem1  31960  dia2dimlem2  31961  dia2dimlem3  31962  dia2dimlem10  31969  dia2dimlem12  31971  cdlemm10N  32014  cdlemn2  32091  cdlemn10  32102  dib2dim  32139  dih2dimb  32140  dih2dimbALTN  32141  dihjatcclem1  32314  dihjatcclem2  32315  dihjatcclem4  32317  dvh4dimat  32334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-sbc 3168  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-mpt 4293  df-id 4527  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-iota 5447  df-fun 5485  df-fv 5491  df-ov 6113  df-lat 14506  df-ats 30163  df-atl 30194  df-cvlat 30218  df-hlat 30247
  Copyright terms: Public domain W3C validator