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

Theorem hlatjcl 35141
Description: Closure of join operation. Frequently-used special case of latjcl 17250 for atoms. (Contributed by NM, 15-Jun-2012.)
Hypotheses
Ref Expression
hlatjcl.b 𝐵 = (Base‘𝐾)
hlatjcl.j = (join‘𝐾)
hlatjcl.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
hlatjcl ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) ∈ 𝐵)

Proof of Theorem hlatjcl
StepHypRef Expression
1 hllat 35137 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐵 = (Base‘𝐾)
3 hlatjcl.a . . 3 𝐴 = (Atoms‘𝐾)
42, 3atbase 35063 . 2 (𝑋𝐴𝑋𝐵)
52, 3atbase 35063 . 2 (𝑌𝐴𝑌𝐵)
6 hlatjcl.j . . 3 = (join‘𝐾)
72, 6latjcl 17250 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
81, 4, 5, 7syl3an 1192 1 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100   = wceq 1637  wcel 2155  cfv 6095  (class class class)co 6868  Basecbs 16062  joincjn 17143  Latclat 17244  Atomscatm 35037  HLchlt 35124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-lub 17173  df-glb 17174  df-join 17175  df-meet 17176  df-lat 17245  df-ats 35041  df-atl 35072  df-cvlat 35096  df-hlat 35125
This theorem is referenced by:  atcvr0eq  35200  2atjm  35219  atbtwn  35220  3dim0  35231  3dimlem3a  35234  3dimlem3OLDN  35236  3dimlem4OLDN  35239  3dim3  35243  2dim  35244  ps-1  35251  hlatexch3N  35254  hlatexch4  35255  ps-2b  35256  3atlem1  35257  3atlem2  35258  llni2  35286  llnle  35292  2at0mat0  35299  2atm  35301  islpln5  35309  lplni2  35311  lplnnle2at  35315  2atnelpln  35318  islpln2a  35322  llncvrlpln2  35331  2atmat  35335  2llnjaN  35340  islvol5  35353  lvoli2  35355  lvolnle3at  35356  3atnelvolN  35360  islvol2aN  35366  4atlem0a  35367  4atlem3  35370  4atlem3a  35371  4atlem3b  35372  4atlem4a  35373  4atlem4b  35374  4atlem4c  35375  4atlem4d  35376  4atlem9  35377  4atlem10a  35378  4atlem10  35380  4atlem11a  35381  4atlem11b  35382  4atlem11  35383  4atlem12a  35384  4atlem12b  35385  4atlem12  35386  4at  35387  4at2  35388  lplncvrlvol2  35389  2lplnja  35393  dalempjqeb  35419  dalemsjteb  35420  dalemtjueb  35421  dalemply  35428  dalem1  35433  dalemcea  35434  dalem3  35438  dalem4  35439  dalem5  35441  dalem-cly  35445  dalem17  35454  dalem21  35468  dalem24  35471  dalem25  35472  dalem27  35473  dalem38  35484  dalem39  35485  dalem43  35489  dalem44  35490  dalem45  35491  dalem55  35501  dalem56  35502  dalem57  35503  2atm2atN  35559  2llnma1b  35560  2llnma3r  35562  llnmod2i2  35637  llnexchb2lem  35642  dalawlem1  35645  dalawlem2  35646  dalawlem3  35647  dalawlem4  35648  dalawlem5  35649  dalawlem6  35650  dalawlem7  35651  dalawlem8  35652  dalawlem9  35653  dalawlem11  35655  dalawlem12  35656  dalawlem15  35659  lhp2lt  35775  lhpexle2lem  35783  lhpexle3lem  35785  lhp2at0  35806  lhp2atnle  35807  lhpat3  35820  4atexlempsb  35834  4atexlemqtb  35835  4atexlemunv  35840  4atexlemtlw  35841  4atexlemc  35843  4atexlemnclw  35844  4atexlemcnd  35846  trlval3  35962  trlval4  35963  cdlemc4  35969  cdlemc5  35970  cdlemc6  35971  cdlemd2  35974  cdleme0e  35992  cdlemeulpq  35995  cdleme01N  35996  cdleme0ex1N  35998  cdleme3g  36009  cdleme3h  36010  cdleme3  36012  cdleme4  36013  cdleme4a  36014  cdleme5  36015  cdleme7aa  36017  cdleme7c  36020  cdleme7d  36021  cdleme7e  36022  cdleme7ga  36023  cdleme7  36024  cdleme9b  36027  cdleme9  36028  cdleme10  36029  cdleme11c  36036  cdleme13  36047  cdleme15b  36050  cdleme15d  36052  cdleme15  36053  cdleme16b  36054  cdleme16e  36057  cdleme16f  36058  cdleme17b  36062  cdleme22gb  36069  cdlemedb  36072  cdlemednpq  36074  cdleme20zN  36076  cdleme19a  36078  cdleme19c  36080  cdleme20aN  36084  cdleme20c  36086  cdleme20d  36087  cdleme20e  36088  cdleme20j  36093  cdleme20l  36097  cdleme21c  36102  cdleme21ct  36104  cdleme22aa  36114  cdleme22b  36116  cdleme22cN  36117  cdleme22d  36118  cdleme22e  36119  cdleme22eALTN  36120  cdleme22f  36121  cdleme22g  36123  cdleme23a  36124  cdleme23b  36125  cdleme23c  36126  cdleme28a  36145  cdleme35a  36223  cdleme35fnpq  36224  cdleme35b  36225  cdleme35c  36226  cdleme35d  36227  cdleme35e  36228  cdleme35f  36229  cdleme42a  36246  cdleme42c  36247  cdleme42h  36257  cdleme42i  36258  cdlemeg46frv  36300  cdlemeg46vrg  36302  cdlemeg46rgv  36303  cdlemeg46req  36304  cdlemf1  36336  cdlemf2  36337  cdlemg2fv2  36375  cdlemg2m  36379  cdlemg4  36392  cdlemg8b  36403  cdlemg10bALTN  36411  cdlemg10c  36414  cdlemg10  36416  cdlemg12e  36422  cdlemg12f  36423  cdlemg12g  36424  cdlemg12  36425  cdlemg13a  36426  cdlemg17a  36436  cdlemg17dALTN  36439  cdlemg17h  36443  cdlemg17  36452  cdlemg18b  36454  cdlemg19a  36458  cdlemg19  36459  cdlemg27a  36467  cdlemg27b  36471  cdlemg31a  36472  cdlemg31b  36473  cdlemg33b0  36476  cdlemg33a  36481  trlcoabs2N  36497  trlcolem  36501  cdlemg42  36504  cdlemg46  36510  cdlemh1  36590  cdlemk3  36608  cdlemk10  36618  cdlemk12  36625  cdlemkole  36628  cdlemk14  36629  cdlemk15  36630  cdlemk1u  36634  cdlemk5u  36636  cdlemk12u  36647  cdlemk37  36689  cdlemk39  36691  cdlemkid1  36697  cdlemk51  36728  cdlemk52  36729  dia2dimlem1  36839  dia2dimlem2  36840  dia2dimlem3  36841  dia2dimlem10  36848  dia2dimlem12  36850  cdlemm10N  36893  cdlemn2  36970  cdlemn10  36981  dib2dim  37018  dih2dimb  37019  dih2dimbALTN  37020  dihjatcclem1  37193  dihjatcclem2  37194  dihjatcclem4  37196  dvh4dimat  37213
  Copyright terms: Public domain W3C validator