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 35174
Description: Closure of join operation. Frequently-used special case of latjcl 17272 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 35171 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐵 = (Base‘𝐾)
3 hlatjcl.a . . 3 𝐴 = (Atoms‘𝐾)
42, 3atbase 35097 . 2 (𝑋𝐴𝑋𝐵)
52, 3atbase 35097 . 2 (𝑌𝐴𝑌𝐵)
6 hlatjcl.j . . 3 = (join‘𝐾)
72, 6latjcl 17272 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
81, 4, 5, 7syl3an 1164 1 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1632  wcel 2139  cfv 6049  (class class class)co 6814  Basecbs 16079  joincjn 17165  Latclat 17266  Atomscatm 35071  HLchlt 35158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-lub 17195  df-glb 17196  df-join 17197  df-meet 17198  df-lat 17267  df-ats 35075  df-atl 35106  df-cvlat 35130  df-hlat 35159
This theorem is referenced by:  atcvr0eq  35233  2atjm  35252  atbtwn  35253  3dim0  35264  3dimlem3a  35267  3dimlem3OLDN  35269  3dimlem4OLDN  35272  3dim3  35276  2dim  35277  ps-1  35284  hlatexch3N  35287  hlatexch4  35288  ps-2b  35289  3atlem1  35290  3atlem2  35291  llni2  35319  llnle  35325  2at0mat0  35332  2atm  35334  islpln5  35342  lplni2  35344  lplnnle2at  35348  2atnelpln  35351  islpln2a  35355  llncvrlpln2  35364  2atmat  35368  2llnjaN  35373  islvol5  35386  lvoli2  35388  lvolnle3at  35389  3atnelvolN  35393  islvol2aN  35399  4atlem0a  35400  4atlem3  35403  4atlem3a  35404  4atlem3b  35405  4atlem4a  35406  4atlem4b  35407  4atlem4c  35408  4atlem4d  35409  4atlem9  35410  4atlem10a  35411  4atlem10  35413  4atlem11a  35414  4atlem11b  35415  4atlem11  35416  4atlem12a  35417  4atlem12b  35418  4atlem12  35419  4at  35420  4at2  35421  lplncvrlvol2  35422  2lplnja  35426  dalempjqeb  35452  dalemsjteb  35453  dalemtjueb  35454  dalemply  35461  dalem1  35466  dalemcea  35467  dalem3  35471  dalem4  35472  dalem5  35474  dalem-cly  35478  dalem17  35487  dalem21  35501  dalem24  35504  dalem25  35505  dalem27  35506  dalem38  35517  dalem39  35518  dalem43  35522  dalem44  35523  dalem45  35524  dalem55  35534  dalem56  35535  dalem57  35536  2atm2atN  35592  2llnma1b  35593  2llnma3r  35595  llnmod2i2  35670  llnexchb2lem  35675  dalawlem1  35678  dalawlem2  35679  dalawlem3  35680  dalawlem4  35681  dalawlem5  35682  dalawlem6  35683  dalawlem7  35684  dalawlem8  35685  dalawlem9  35686  dalawlem11  35688  dalawlem12  35689  dalawlem15  35692  lhp2lt  35808  lhpexle2lem  35816  lhpexle3lem  35818  lhp2at0  35839  lhp2atnle  35840  lhpat3  35853  4atexlempsb  35867  4atexlemqtb  35868  4atexlemunv  35873  4atexlemtlw  35874  4atexlemc  35876  4atexlemnclw  35877  4atexlemcnd  35879  trlval3  35995  trlval4  35996  cdlemc4  36002  cdlemc5  36003  cdlemc6  36004  cdlemd2  36007  cdleme0e  36025  cdlemeulpq  36028  cdleme01N  36029  cdleme0ex1N  36031  cdleme3g  36042  cdleme3h  36043  cdleme3  36045  cdleme4  36046  cdleme4a  36047  cdleme5  36048  cdleme7aa  36050  cdleme7c  36053  cdleme7d  36054  cdleme7e  36055  cdleme7ga  36056  cdleme7  36057  cdleme9b  36060  cdleme9  36061  cdleme10  36062  cdleme11c  36069  cdleme13  36080  cdleme15b  36083  cdleme15d  36085  cdleme15  36086  cdleme16b  36087  cdleme16e  36090  cdleme16f  36091  cdleme17b  36095  cdleme22gb  36102  cdlemedb  36105  cdlemednpq  36107  cdleme20zN  36109  cdleme19a  36111  cdleme19c  36113  cdleme20aN  36117  cdleme20c  36119  cdleme20d  36120  cdleme20e  36121  cdleme20j  36126  cdleme20l  36130  cdleme21c  36135  cdleme21ct  36137  cdleme22aa  36147  cdleme22b  36149  cdleme22cN  36150  cdleme22d  36151  cdleme22e  36152  cdleme22eALTN  36153  cdleme22f  36154  cdleme22g  36156  cdleme23a  36157  cdleme23b  36158  cdleme23c  36159  cdleme28a  36178  cdleme35a  36256  cdleme35fnpq  36257  cdleme35b  36258  cdleme35c  36259  cdleme35d  36260  cdleme35e  36261  cdleme35f  36262  cdleme42a  36279  cdleme42c  36280  cdleme42h  36290  cdleme42i  36291  cdlemeg46frv  36333  cdlemeg46vrg  36335  cdlemeg46rgv  36336  cdlemeg46req  36337  cdlemf1  36369  cdlemf2  36370  cdlemg2fv2  36408  cdlemg2m  36412  cdlemg4  36425  cdlemg8b  36436  cdlemg10bALTN  36444  cdlemg10c  36447  cdlemg10  36449  cdlemg12e  36455  cdlemg12f  36456  cdlemg12g  36457  cdlemg12  36458  cdlemg13a  36459  cdlemg17a  36469  cdlemg17dALTN  36472  cdlemg17h  36476  cdlemg17  36485  cdlemg18b  36487  cdlemg19a  36491  cdlemg19  36492  cdlemg27a  36500  cdlemg27b  36504  cdlemg31a  36505  cdlemg31b  36506  cdlemg33b0  36509  cdlemg33a  36514  trlcoabs2N  36530  trlcolem  36534  cdlemg42  36537  cdlemg46  36543  cdlemh1  36623  cdlemk3  36641  cdlemk10  36651  cdlemk12  36658  cdlemkole  36661  cdlemk14  36662  cdlemk15  36663  cdlemk1u  36667  cdlemk5u  36669  cdlemk12u  36680  cdlemk37  36722  cdlemk39  36724  cdlemkid1  36730  cdlemk51  36761  cdlemk52  36762  dia2dimlem1  36873  dia2dimlem2  36874  dia2dimlem3  36875  dia2dimlem10  36882  dia2dimlem12  36884  cdlemm10N  36927  cdlemn2  37004  cdlemn10  37015  dib2dim  37052  dih2dimb  37053  dih2dimbALTN  37054  dihjatcclem1  37227  dihjatcclem2  37228  dihjatcclem4  37230  dvh4dimat  37247
  Copyright terms: Public domain W3C validator