Theorem chsh 31516

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

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913   “ cima 5665  (class class class)co 7411   ↑_m cmap 8823  ℕcn 12232   ⇝_𝑣 chli 31219   S_ℋ csh 31220   C_ℋ cch 31221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fv 6545  df-ov 7414  df-ch 31513

This theorem is referenced by:  chsssh  31517  chshii  31519  ch0  31520  chss  31521  choccl  31598  chjval  31644  chjcl  31649  pjhth  31685  pjhtheu  31686  pjpreeq  31690  pjpjpre  31711  ch0le  31733  chle0  31735  chslej  31790  chjcom  31798  chub1  31799  chlub  31801  chlej1  31802  chlej2  31803  spansnsh  31853  fh1  31910  fh2  31911  chscllem1  31929  chscllem2  31930  chscllem3  31931  chscllem4  31932  chscl  31933  pjorthi  31961  pjoi0  32009  hstoc  32514  hstnmoc  32515  ch1dle  32644  atomli  32674  chirredlem3  32684  sumdmdii  32707