Theorem chsh 31576

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905   “ cima 5664  (class class class)co 7410   ↑_m cmap 8820  ℕcn 12228   ⇝_𝑣 chli 31279   S_ℋ csh 31280   C_ℋ cch 31281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fv 6544  df-ov 7413  df-ch 31573

This theorem is referenced by:  chsssh  31577  chshii  31579  ch0  31580  chss  31581  choccl  31658  chjval  31704  chjcl  31709  pjhth  31745  pjhtheu  31746  pjpreeq  31750  pjpjpre  31771  ch0le  31793  chle0  31795  chslej  31850  chjcom  31858  chub1  31859  chlub  31861  chlej1  31862  chlej2  31863  spansnsh  31913  fh1  31970  fh2  31971  chscllem1  31989  chscllem2  31990  chscllem3  31991  chscllem4  31992  chscl  31993  pjorthi  32021  pjoi0  32069  hstoc  32574  hstnmoc  32575  ch1dle  32704  atomli  32734  chirredlem3  32744  sumdmdii  32767