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 36389
Description: Closure of join operation. Frequently-used special case of latjcl 17656 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 36385 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐵 = (Base‘𝐾)
3 hlatjcl.a . . 3 𝐴 = (Atoms‘𝐾)
42, 3atbase 36311 . 2 (𝑋𝐴𝑋𝐵)
52, 3atbase 36311 . 2 (𝑌𝐴𝑌𝐵)
6 hlatjcl.j . . 3 = (join‘𝐾)
72, 6latjcl 17656 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
81, 4, 5, 7syl3an 1154 1 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081   = wceq 1530  wcel 2107  cfv 6354  (class class class)co 7150  Basecbs 16478  joincjn 17549  Latclat 17650  Atomscatm 36285  HLchlt 36372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-lat 17651  df-ats 36289  df-atl 36320  df-cvlat 36344  df-hlat 36373
This theorem is referenced by:  atcvr0eq  36448  2atjm  36467  atbtwn  36468  3dim0  36479  3dimlem3a  36482  3dimlem3OLDN  36484  3dimlem4OLDN  36487  3dim3  36491  2dim  36492  ps-1  36499  hlatexch3N  36502  hlatexch4  36503  ps-2b  36504  3atlem1  36505  3atlem2  36506  llni2  36534  llnle  36540  2at0mat0  36547  2atm  36549  islpln5  36557  lplni2  36559  lplnnle2at  36563  2atnelpln  36566  islpln2a  36570  llncvrlpln2  36579  2atmat  36583  2llnjaN  36588  islvol5  36601  lvoli2  36603  lvolnle3at  36604  3atnelvolN  36608  islvol2aN  36614  4atlem0a  36615  4atlem3  36618  4atlem3a  36619  4atlem3b  36620  4atlem4a  36621  4atlem4b  36622  4atlem4c  36623  4atlem4d  36624  4atlem9  36625  4atlem10a  36626  4atlem10  36628  4atlem11a  36629  4atlem11b  36630  4atlem11  36631  4atlem12a  36632  4atlem12b  36633  4atlem12  36634  4at  36635  4at2  36636  lplncvrlvol2  36637  2lplnja  36641  dalempjqeb  36667  dalemsjteb  36668  dalemtjueb  36669  dalemply  36676  dalem1  36681  dalemcea  36682  dalem3  36686  dalem4  36687  dalem5  36689  dalem-cly  36693  dalem17  36702  dalem21  36716  dalem24  36719  dalem25  36720  dalem27  36721  dalem38  36732  dalem39  36733  dalem43  36737  dalem44  36738  dalem45  36739  dalem55  36749  dalem56  36750  dalem57  36751  2atm2atN  36807  2llnma1b  36808  2llnma3r  36810  llnmod2i2  36885  llnexchb2lem  36890  dalawlem1  36893  dalawlem2  36894  dalawlem3  36895  dalawlem4  36896  dalawlem5  36897  dalawlem6  36898  dalawlem7  36899  dalawlem8  36900  dalawlem9  36901  dalawlem11  36903  dalawlem12  36904  dalawlem15  36907  lhp2lt  37023  lhpexle2lem  37031  lhpexle3lem  37033  lhp2at0  37054  lhp2atnle  37055  lhpat3  37068  4atexlempsb  37082  4atexlemqtb  37083  4atexlemunv  37088  4atexlemtlw  37089  4atexlemc  37091  4atexlemnclw  37092  4atexlemcnd  37094  trlval3  37209  trlval4  37210  cdlemc4  37216  cdlemc5  37217  cdlemc6  37218  cdlemd2  37221  cdleme0e  37239  cdlemeulpq  37242  cdleme01N  37243  cdleme0ex1N  37245  cdleme3g  37256  cdleme3h  37257  cdleme3  37259  cdleme4  37260  cdleme4a  37261  cdleme5  37262  cdleme7aa  37264  cdleme7c  37267  cdleme7d  37268  cdleme7e  37269  cdleme7ga  37270  cdleme7  37271  cdleme9b  37274  cdleme9  37275  cdleme10  37276  cdleme11c  37283  cdleme13  37294  cdleme15b  37297  cdleme15d  37299  cdleme15  37300  cdleme16b  37301  cdleme16e  37304  cdleme16f  37305  cdleme17b  37309  cdleme22gb  37316  cdlemedb  37319  cdlemednpq  37321  cdleme20zN  37323  cdleme19a  37325  cdleme19c  37327  cdleme20aN  37331  cdleme20c  37333  cdleme20d  37334  cdleme20e  37335  cdleme20j  37340  cdleme20l  37344  cdleme21c  37349  cdleme21ct  37351  cdleme22aa  37361  cdleme22b  37363  cdleme22cN  37364  cdleme22d  37365  cdleme22e  37366  cdleme22eALTN  37367  cdleme22f  37368  cdleme22g  37370  cdleme23a  37371  cdleme23b  37372  cdleme23c  37373  cdleme28a  37392  cdleme35a  37470  cdleme35fnpq  37471  cdleme35b  37472  cdleme35c  37473  cdleme35d  37474  cdleme35e  37475  cdleme35f  37476  cdleme42a  37493  cdleme42c  37494  cdleme42h  37504  cdleme42i  37505  cdlemeg46frv  37547  cdlemeg46vrg  37549  cdlemeg46rgv  37550  cdlemeg46req  37551  cdlemf1  37583  cdlemf2  37584  cdlemg2fv2  37622  cdlemg2m  37626  cdlemg4  37639  cdlemg8b  37650  cdlemg10bALTN  37658  cdlemg10c  37661  cdlemg10  37663  cdlemg12e  37669  cdlemg12f  37670  cdlemg12g  37671  cdlemg12  37672  cdlemg13a  37673  cdlemg17a  37683  cdlemg17dALTN  37686  cdlemg17h  37690  cdlemg17  37699  cdlemg18b  37701  cdlemg19a  37705  cdlemg19  37706  cdlemg27a  37714  cdlemg27b  37718  cdlemg31a  37719  cdlemg31b  37720  cdlemg33b0  37723  cdlemg33a  37728  trlcoabs2N  37744  trlcolem  37748  cdlemg42  37751  cdlemg46  37757  cdlemh1  37837  cdlemk3  37855  cdlemk10  37865  cdlemk12  37872  cdlemkole  37875  cdlemk14  37876  cdlemk15  37877  cdlemk1u  37881  cdlemk5u  37883  cdlemk12u  37894  cdlemk37  37936  cdlemk39  37938  cdlemkid1  37944  cdlemk51  37975  cdlemk52  37976  dia2dimlem1  38086  dia2dimlem2  38087  dia2dimlem3  38088  dia2dimlem10  38095  dia2dimlem12  38097  cdlemm10N  38140  cdlemn2  38217  cdlemn10  38228  dib2dim  38265  dih2dimb  38266  dih2dimbALTN  38267  dihjatcclem1  38440  dihjatcclem2  38441  dihjatcclem4  38443  dvh4dimat  38460
  Copyright terms: Public domain W3C validator