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

Theorem hlatjcl 30003
Description: Closure of join operation. Frequently-used special case of latjcl 14467 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 30000 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 hlatjcl.b . . 3  |-  B  =  ( Base `  K
)
3 hlatjcl.a . . 3  |-  A  =  ( Atoms `  K )
42, 3atbase 29926 . 2  |-  ( X  e.  A  ->  X  e.  B )
52, 3atbase 29926 . 2  |-  ( Y  e.  A  ->  Y  e.  B )
6 hlatjcl.j . . 3  |-  .\/  =  ( join `  K )
72, 6latjcl 14467 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
81, 4, 5, 7syl3an 1226 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 936    = wceq 1652    e. wcel 1725   ` cfv 5445  (class class class)co 6072   Basecbs 13457   joincjn 14389   Latclat 14462   Atomscatm 29900   HLchlt 29987
This theorem is referenced by:  atcvr0eq  30062  2atjm  30081  atbtwn  30082  3dim0  30093  3dimlem3a  30096  3dimlem3OLDN  30098  3dimlem4OLDN  30101  3dim3  30105  2dim  30106  ps-1  30113  hlatexch3N  30116  hlatexch4  30117  ps-2b  30118  3atlem1  30119  3atlem2  30120  llni2  30148  llnle  30154  2at0mat0  30161  2atm  30163  islpln5  30171  lplni2  30173  lplnnle2at  30177  2atnelpln  30180  islpln2a  30184  llncvrlpln2  30193  2atmat  30197  2llnjaN  30202  islvol5  30215  lvoli2  30217  lvolnle3at  30218  3atnelvolN  30222  islvol2aN  30228  4atlem0a  30229  4atlem3  30232  4atlem3a  30233  4atlem3b  30234  4atlem4a  30235  4atlem4b  30236  4atlem4c  30237  4atlem4d  30238  4atlem9  30239  4atlem10a  30240  4atlem10  30242  4atlem11a  30243  4atlem11b  30244  4atlem11  30245  4atlem12a  30246  4atlem12b  30247  4atlem12  30248  4at  30249  4at2  30250  lplncvrlvol2  30251  2lplnja  30255  dalempjqeb  30281  dalemsjteb  30282  dalemtjueb  30283  dalemply  30290  dalem1  30295  dalemcea  30296  dalem3  30300  dalem4  30301  dalem5  30303  dalem-cly  30307  dalem17  30316  dalem21  30330  dalem24  30333  dalem25  30334  dalem27  30335  dalem38  30346  dalem39  30347  dalem43  30351  dalem44  30352  dalem45  30353  dalem55  30363  dalem56  30364  dalem57  30365  2atm2atN  30421  2llnma1b  30422  2llnma3r  30424  llnmod2i2  30499  llnexchb2lem  30504  dalawlem1  30507  dalawlem2  30508  dalawlem3  30509  dalawlem4  30510  dalawlem5  30511  dalawlem6  30512  dalawlem7  30513  dalawlem8  30514  dalawlem9  30515  dalawlem11  30517  dalawlem12  30518  dalawlem15  30521  lhp2lt  30637  lhpexle2lem  30645  lhpexle3lem  30647  lhp2at0  30668  lhp2atnle  30669  lhpat3  30682  4atexlempsb  30696  4atexlemqtb  30697  4atexlemunv  30702  4atexlemtlw  30703  4atexlemc  30705  4atexlemnclw  30706  4atexlemcnd  30708  trlval3  30823  trlval4  30824  cdlemc4  30830  cdlemc5  30831  cdlemc6  30832  cdlemd2  30835  cdleme0e  30853  cdlemeulpq  30856  cdleme01N  30857  cdleme0ex1N  30859  cdleme3g  30870  cdleme3h  30871  cdleme3  30873  cdleme4  30874  cdleme4a  30875  cdleme5  30876  cdleme7aa  30878  cdleme7c  30881  cdleme7d  30882  cdleme7e  30883  cdleme7ga  30884  cdleme7  30885  cdleme9b  30888  cdleme9  30889  cdleme10  30890  cdleme11c  30897  cdleme13  30908  cdleme15b  30911  cdleme15d  30913  cdleme15  30914  cdleme16b  30915  cdleme16e  30918  cdleme16f  30919  cdleme17b  30923  cdleme22gb  30930  cdlemedb  30933  cdlemednpq  30935  cdleme20zN  30937  cdleme20y  30938  cdleme19a  30939  cdleme19c  30941  cdleme20aN  30945  cdleme20c  30947  cdleme20d  30948  cdleme20e  30949  cdleme20j  30954  cdleme20l  30958  cdleme21c  30963  cdleme21ct  30965  cdleme22aa  30975  cdleme22b  30977  cdleme22cN  30978  cdleme22d  30979  cdleme22e  30980  cdleme22eALTN  30981  cdleme22f  30982  cdleme22g  30984  cdleme23a  30985  cdleme23b  30986  cdleme23c  30987  cdleme28a  31006  cdleme35a  31084  cdleme35fnpq  31085  cdleme35b  31086  cdleme35c  31087  cdleme35d  31088  cdleme35e  31089  cdleme35f  31090  cdleme42a  31107  cdleme42c  31108  cdleme42h  31118  cdleme42i  31119  cdlemeg46frv  31161  cdlemeg46vrg  31163  cdlemeg46rgv  31164  cdlemeg46req  31165  cdlemf1  31197  cdlemf2  31198  cdlemg2fv2  31236  cdlemg2m  31240  cdlemg4  31253  cdlemg8b  31264  cdlemg10bALTN  31272  cdlemg10c  31275  cdlemg10  31277  cdlemg12e  31283  cdlemg12f  31284  cdlemg12g  31285  cdlemg12  31286  cdlemg13a  31287  cdlemg17a  31297  cdlemg17dALTN  31300  cdlemg17h  31304  cdlemg17  31313  cdlemg18b  31315  cdlemg19a  31319  cdlemg19  31320  cdlemg27a  31328  cdlemg27b  31332  cdlemg31a  31333  cdlemg31b  31334  cdlemg33b0  31337  cdlemg33a  31342  trlcoabs2N  31358  trlcolem  31362  cdlemg42  31365  cdlemg46  31371  cdlemh1  31451  cdlemk3  31469  cdlemk10  31479  cdlemk12  31486  cdlemkole  31489  cdlemk14  31490  cdlemk15  31491  cdlemk1u  31495  cdlemk5u  31497  cdlemk12u  31508  cdlemk37  31550  cdlemk39  31552  cdlemkid1  31558  cdlemk51  31589  cdlemk52  31590  dia2dimlem1  31701  dia2dimlem2  31702  dia2dimlem3  31703  dia2dimlem10  31710  dia2dimlem12  31712  cdlemm10N  31755  cdlemn2  31832  cdlemn10  31843  dib2dim  31880  dih2dimb  31881  dih2dimbALTN  31882  dihjatcclem1  32055  dihjatcclem2  32056  dihjatcclem4  32058  dvh4dimat  32075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-iota 5409  df-fun 5447  df-fv 5453  df-ov 6075  df-lat 14463  df-ats 29904  df-atl 29935  df-cvlat 29959  df-hlat 29988
  Copyright terms: Public domain W3C validator