Theorem chsh 31313

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	⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )

Proof of Theorem chsh

Step	Hyp	Ref	Expression
1		isch 31311	. 2 ⊢ (𝐻 ∈ Cℋ ↔ (𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ (𝐻 ↑m ℕ)) ⊆ 𝐻))
2	1	simplbi 497	1 ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883   “ cima 5621  (class class class)co 7356   ↑_m cmap 8763  ℕcn 12165   ⇝_𝑣 chli 31016   S_ℋ csh 31017   C_ℋ cch 31018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fv 6493  df-ov 7359  df-ch 31310

This theorem is referenced by:  chsssh  31314  chshii  31316  ch0  31317  chss  31318  choccl  31395  chjval  31441  chjcl  31446  pjhth  31482  pjhtheu  31483  pjpreeq  31487  pjpjpre  31508  ch0le  31530  chle0  31532  chslej  31587  chjcom  31595  chub1  31596  chlub  31598  chlej1  31599  chlej2  31600  spansnsh  31650  fh1  31707  fh2  31708  chscllem1  31726  chscllem2  31727  chscllem3  31728  chscllem4  31729  chscl  31730  pjorthi  31758  pjoi0  31806  hstoc  32311  hstnmoc  32312  ch1dle  32441  atomli  32471  chirredlem3  32481  sumdmdii  32504