Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlatjcl Structured version   Unicode version
Theorem hlatjcl 34564
Description: Closure of join operation. Frequently-used special case of latjcl 15555 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 34561 . 2 |- ( K e. HL -> K e. Lat )
2 hlatjcl.b . . 3 |- B = ( Base ` K )
3 hlatjcl.a . . 3 |- A = ( Atoms ` K )
42, 3atbase 34487 . 2 |- ( X e. A -> X e. B )
52, 3atbase 34487 . 2 |- ( Y e. A -> Y e. B )
6 hlatjcl.j . . 3 |- .\/ = ( join ` K )
72, 6latjcl 15555 . 2 |- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
81, 4, 5, 7syl3an 1270 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 973   = wceq 1379   e. wcel 1767   ` cfv 5594  (class class class)co 6295   Basecbs 14507   joincjn 15448   Latclat 15549   Atomscatm 34461   HLchlt 34548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-lub 15478  df-glb 15479  df-join 15480  df-meet 15481  df-lat 15550  df-ats 34465  df-atl 34496  df-cvlat 34520  df-hlat 34549
This theorem is referenced by:  atcvr0eq  34623  2atjm  34642  atbtwn  34643  3dim0  34654  3dimlem3a  34657  3dimlem3OLDN  34659  3dimlem4OLDN  34662  3dim3  34666  2dim  34667  ps-1  34674  hlatexch3N  34677  hlatexch4  34678  ps-2b  34679  3atlem1  34680  3atlem2  34681  llni2  34709  llnle  34715  2at0mat0  34722  2atm  34724  islpln5  34732  lplni2  34734  lplnnle2at  34738  2atnelpln  34741  islpln2a  34745  llncvrlpln2  34754  2atmat  34758  2llnjaN  34763  islvol5  34776  lvoli2  34778  lvolnle3at  34779  3atnelvolN  34783  islvol2aN  34789  4atlem0a  34790  4atlem3  34793  4atlem3a  34794  4atlem3b  34795  4atlem4a  34796  4atlem4b  34797  4atlem4c  34798  4atlem4d  34799  4atlem9  34800  4atlem10a  34801  4atlem10  34803  4atlem11a  34804  4atlem11b  34805  4atlem11  34806  4atlem12a  34807  4atlem12b  34808  4atlem12  34809  4at  34810  4at2  34811  lplncvrlvol2  34812  2lplnja  34816  dalempjqeb  34842  dalemsjteb  34843  dalemtjueb  34844  dalemply  34851  dalem1  34856  dalemcea  34857  dalem3  34861  dalem4  34862  dalem5  34864  dalem-cly  34868  dalem17  34877  dalem21  34891  dalem24  34894  dalem25  34895  dalem27  34896  dalem38  34907  dalem39  34908  dalem43  34912  dalem44  34913  dalem45  34914  dalem55  34924  dalem56  34925  dalem57  34926  2atm2atN  34982  2llnma1b  34983  2llnma3r  34985  llnmod2i2  35060  llnexchb2lem  35065  dalawlem1  35068  dalawlem2  35069  dalawlem3  35070  dalawlem4  35071  dalawlem5  35072  dalawlem6  35073  dalawlem7  35074  dalawlem8  35075  dalawlem9  35076  dalawlem11  35078  dalawlem12  35079  dalawlem15  35082  lhp2lt  35198  lhpexle2lem  35206  lhpexle3lem  35208  lhp2at0  35229  lhp2atnle  35230  lhpat3  35243  4atexlempsb  35257  4atexlemqtb  35258  4atexlemunv  35263  4atexlemtlw  35264  4atexlemc  35266  4atexlemnclw  35267  4atexlemcnd  35269  trlval3  35384  trlval4  35385  cdlemc4  35391  cdlemc5  35392  cdlemc6  35393  cdlemd2  35396  cdleme0e  35414  cdlemeulpq  35417  cdleme01N  35418  cdleme0ex1N  35420  cdleme3g  35431  cdleme3h  35432  cdleme3  35434  cdleme4  35435  cdleme4a  35436  cdleme5  35437  cdleme7aa  35439  cdleme7c  35442  cdleme7d  35443  cdleme7e  35444  cdleme7ga  35445  cdleme7  35446  cdleme9b  35449  cdleme9  35450  cdleme10  35451  cdleme11c  35458  cdleme13  35469  cdleme15b  35472  cdleme15d  35474  cdleme15  35475  cdleme16b  35476  cdleme16e  35479  cdleme16f  35480  cdleme17b  35484  cdleme22gb  35491  cdlemedb  35494  cdlemednpq  35496  cdleme20zN  35498  cdleme20y  35499  cdleme19a  35500  cdleme19c  35502  cdleme20aN  35506  cdleme20c  35508  cdleme20d  35509  cdleme20e  35510  cdleme20j  35515  cdleme20l  35519  cdleme21c  35524  cdleme21ct  35526  cdleme22aa  35536  cdleme22b  35538  cdleme22cN  35539  cdleme22d  35540  cdleme22e  35541  cdleme22eALTN  35542  cdleme22f  35543  cdleme22g  35545  cdleme23a  35546  cdleme23b  35547  cdleme23c  35548  cdleme28a  35567  cdleme35a  35645  cdleme35fnpq  35646  cdleme35b  35647  cdleme35c  35648  cdleme35d  35649  cdleme35e  35650  cdleme35f  35651  cdleme42a  35668  cdleme42c  35669  cdleme42h  35679  cdleme42i  35680  cdlemeg46frv  35722  cdlemeg46vrg  35724  cdlemeg46rgv  35725  cdlemeg46req  35726  cdlemf1  35758  cdlemf2  35759  cdlemg2fv2  35797  cdlemg2m  35801  cdlemg4  35814  cdlemg8b  35825  cdlemg10bALTN  35833  cdlemg10c  35836  cdlemg10  35838  cdlemg12e  35844  cdlemg12f  35845  cdlemg12g  35846  cdlemg12  35847  cdlemg13a  35848  cdlemg17a  35858  cdlemg17dALTN  35861  cdlemg17h  35865  cdlemg17  35874  cdlemg18b  35876  cdlemg19a  35880  cdlemg19  35881  cdlemg27a  35889  cdlemg27b  35893  cdlemg31a  35894  cdlemg31b  35895  cdlemg33b0  35898  cdlemg33a  35903  trlcoabs2N  35919  trlcolem  35923  cdlemg42  35926  cdlemg46  35932  cdlemh1  36012  cdlemk3  36030  cdlemk10  36040  cdlemk12  36047  cdlemkole  36050  cdlemk14  36051  cdlemk15  36052  cdlemk1u  36056  cdlemk5u  36058  cdlemk12u  36069  cdlemk37  36111  cdlemk39  36113  cdlemkid1  36119  cdlemk51  36150  cdlemk52  36151  dia2dimlem1  36262  dia2dimlem2  36263  dia2dimlem3  36264  dia2dimlem10  36271  dia2dimlem12  36273  cdlemm10N  36316  cdlemn2  36393  cdlemn10  36404  dib2dim  36441  dih2dimb  36442  dih2dimbALTN  36443  dihjatcclem1  36616  dihjatcclem2  36617  dihjatcclem4  36619  dvh4dimat  36636
  Copyright terms: Public domain W3C validator