Theorem chsh 28081

Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
chsh	|- ( H e. CH -> H e. SH )

Proof of Theorem chsh

Step	Hyp	Ref	Expression
1		isch 28079	. 2 |- ( H e. CH <-> ( H e. SH /\ ( ~~>v " ( H ^m NN ) ) C_ H ) )
2	1	simplbi 476	1 |- ( H e. CH -> H e. SH )

Syntax hints:   -> wi 4   e. wcel 1990   C_ wss 3574   "cima 5117  (class class class)co 6650   ^m cmap 7857   NNcn 11020   ~~>v chli 27784   SHcsh 27785   CHcch 27786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fv 5896  df-ov 6653  df-ch 28078

This theorem is referenced by:  chsssh  28082  chshii  28084  ch0  28085  chss  28086  choccl  28165  chjval  28211  chjcl  28216  pjhth  28252  pjhtheu  28253  pjpreeq  28257  pjpjpre  28278  ch0le  28300  chle0  28302  chslej  28357  chjcom  28365  chub1  28366  chlub  28368  chlej1  28369  chlej2  28370  spansnsh  28420  fh1  28477  fh2  28478  chscllem1  28496  chscllem2  28497  chscllem3  28498  chscllem4  28499  chscl  28500  pjorthi  28528  pjoi0  28576  hstoc  29081  hstnmoc  29082  ch1dle  29211  atomli  29241  chirredlem3  29251  sumdmdii  29274