Theorem chsh 31312

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 31310	. 2 ⊢ (𝐻 ∈ Cℋ ↔ (𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ (𝐻 ↑m ℕ)) ⊆ 𝐻))
2	1	simplbi 496	1 ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903   “ cima 5635  (class class class)co 7368   ↑_m cmap 8775  ℕcn 12157   ⇝_𝑣 chli 31015   S_ℋ csh 31016   C_ℋ cch 31017

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fv 6508  df-ov 7371  df-ch 31309

This theorem is referenced by:  chsssh  31313  chshii  31315  ch0  31316  chss  31317  choccl  31394  chjval  31440  chjcl  31445  pjhth  31481  pjhtheu  31482  pjpreeq  31486  pjpjpre  31507  ch0le  31529  chle0  31531  chslej  31586  chjcom  31594  chub1  31595  chlub  31597  chlej1  31598  chlej2  31599  spansnsh  31649  fh1  31706  fh2  31707  chscllem1  31725  chscllem2  31726  chscllem3  31727  chscllem4  31728  chscl  31729  pjorthi  31757  pjoi0  31805  hstoc  32310  hstnmoc  32311  ch1dle  32440  atomli  32470  chirredlem3  32480  sumdmdii  32503