Theorem chsh 31706

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899   “ cima 5658  (class class class)co 7414   ↑_m cmap 8827  ℕcn 12258   ⇝_𝑣 chli 31409   S_ℋ csh 31410   C_ℋ cch 31411

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fv 6541  df-ov 7417  df-ch 31703

This theorem is used by:  chsssh  31707  chshii  31709  ch0  31710  chss  31711  choccl  31788  chjval  31834  chjcl  31839  pjhth  31875  pjhtheu  31876  pjpreeq  31880  pjpjpre  31901  ch0le  31923  chle0  31925  chslej  31980  chjcom  31988  chub1  31989  chlub  31991  chlej1  31992  chlej2  31993  spansnsh  32043  fh1  32100  fh2  32101  chscllem1  32119  chscllem2  32120  chscllem3  32121  chscllem4  32122  chscl  32123  pjorthi  32151  pjoi0  32199  hstoc  32704  hstnmoc  32705  ch1dle  32834  atomli  32864  chirredlem3  32874  sumdmdii  32897