HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  chjcl Unicode version

Theorem chjcl 21932
Description: Closure of join in  CH. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
Assertion
Ref Expression
chjcl  |-  ( ( A  e.  CH  /\  B  e.  CH )  ->  ( A  vH  B
)  e.  CH )

Proof of Theorem chjcl
StepHypRef Expression
1 chsh 21800 . 2  |-  ( A  e.  CH  ->  A  e.  SH )
2 chsh 21800 . 2  |-  ( B  e.  CH  ->  B  e.  SH )
3 shjcl 21931 . 2  |-  ( ( A  e.  SH  /\  B  e.  SH )  ->  ( A  vH  B
)  e.  CH )
41, 2, 3syl2an 463 1  |-  ( ( A  e.  CH  /\  B  e.  CH )  ->  ( A  vH  B
)  e.  CH )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1685  (class class class)co 5820   SHcsh 21504   CHcch 21505    vH chj 21509
This theorem is referenced by:  chj4  22110  cm0  22184  pjoml5  22188  fh1  22193  fh2  22194  cm2j  22195  spansnscl  22223  hstle  22806  strlem3a  22828  hstrlem3a  22836  spansncv2  22869  mdbr2  22872  dmdmd  22876  dmdbr3  22881  dmdbr4  22882  dmdbr5  22884  mdsl1i  22897  mdsl2i  22898  mdslmd1i  22905  mdexchi  22911  cvdmd  22913  chcv1  22931  cvati  22942  cvexchlem  22944  atcv0eq  22955  atexch  22957  atomli  22958  atcvatlem  22961  atcvat2i  22963  chirredlem3  22968  atcvat3i  22972  atcvat4i  22973  mdsymlem1  22979  mdsymlem3  22981  mdsymlem5  22983  mdsymlem6  22984  dmdbr5ati  22998
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-inf2 7338  ax-cnex 8789  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-mulcom 8797  ax-addass 8798  ax-mulass 8799  ax-distr 8800  ax-i2m1 8801  ax-1ne0 8802  ax-1rid 8803  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807  ax-pre-lttrn 8808  ax-pre-ltadd 8809  ax-pre-mulgt0 8810  ax-pre-sup 8811  ax-addf 8812  ax-mulf 8813  ax-hilex 21575  ax-hfvadd 21576  ax-hvcom 21577  ax-hvass 21578  ax-hv0cl 21579  ax-hvaddid 21580  ax-hfvmul 21581  ax-hvmulid 21582  ax-hvmulass 21583  ax-hvdistr1 21584  ax-hvdistr2 21585  ax-hvmul0 21586  ax-hfi 21654  ax-his1 21657  ax-his2 21658  ax-his3 21659  ax-his4 21660  ax-hcompl 21777
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rmo 2552  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-iun 3908  df-iin 3909  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-se 4352  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-isom 5230  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-of 6040  df-1st 6084  df-2nd 6085  df-iota 6253  df-riota 6300  df-recs 6384  df-rdg 6419  df-1o 6475  df-2o 6476  df-oadd 6479  df-er 6656  df-map 6770  df-pm 6771  df-ixp 6814  df-en 6860  df-dom 6861  df-sdom 6862  df-fin 6863  df-fi 7161  df-sup 7190  df-oi 7221  df-card 7568  df-cda 7790  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869  df-sub 9035  df-neg 9036  df-div 9420  df-nn 9743  df-2 9800  df-3 9801  df-4 9802  df-5 9803  df-6 9804  df-7 9805  df-8 9806  df-9 9807  df-10 9808  df-n0 9962  df-z 10021  df-dec 10121  df-uz 10227  df-q 10313  df-rp 10351  df-xneg 10448  df-xadd 10449  df-xmul 10450  df-ioo 10656  df-icc 10659  df-fz 10779  df-fzo 10867  df-seq 11043  df-exp 11101  df-hash 11334  df-cj 11580  df-re 11581  df-im 11582  df-sqr 11716  df-abs 11717  df-clim 11958  df-sum 12155  df-struct 13146  df-ndx 13147  df-slot 13148  df-base 13149  df-sets 13150  df-ress 13151  df-plusg 13217  df-mulr 13218  df-starv 13219  df-sca 13220  df-vsca 13221  df-tset 13223  df-ple 13224  df-ds 13226  df-hom 13228  df-cco 13229  df-rest 13323  df-topn 13324  df-topgen 13340  df-pt 13341  df-prds 13344  df-xrs 13399  df-0g 13400  df-gsum 13401  df-qtop 13406  df-imas 13407  df-xps 13409  df-mre 13484  df-mrc 13485  df-acs 13487  df-mnd 14363  df-submnd 14412  df-mulg 14488  df-cntz 14789  df-cmn 15087  df-xmet 16369  df-met 16370  df-bl 16371  df-mopn 16372  df-cnfld 16374  df-top 16632  df-bases 16634  df-topon 16635  df-topsp 16636  df-cn 16953  df-cnp 16954  df-lm 16955  df-haus 17039  df-tx 17253  df-hmeo 17442  df-xms 17881  df-ms 17882  df-tms 17883  df-cau 18678  df-grpo 20852  df-gid 20853  df-ginv 20854  df-gdiv 20855  df-ablo 20943  df-vc 21096  df-nv 21142  df-va 21145  df-ba 21146  df-sm 21147  df-0v 21148  df-vs 21149  df-nmcv 21150  df-ims 21151  df-dip 21268  df-hnorm 21544  df-hvsub 21547  df-hlim 21548  df-hcau 21549  df-sh 21782  df-ch 21797  df-oc 21827  df-chj 21885
  Copyright terms: Public domain W3C validator