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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890   “ cima 5628  (class class class)co 7361   ↑_m cmap 8767  ℕcn 12168   ⇝_𝑣 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fv 6501  df-ov 7364  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