Theorem chsh 29007

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881   “ cima 5522  (class class class)co 7135   ↑_m cmap 8389  ℕcn 11625   ⇝_𝑣 chli 28710   S_ℋ csh 28711   C_ℋ cch 28712

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fv 6332  df-ov 7138  df-ch 29004

This theorem is referenced by:  chsssh  29008  chshii  29010  ch0  29011  chss  29012  choccl  29089  chjval  29135  chjcl  29140  pjhth  29176  pjhtheu  29177  pjpreeq  29181  pjpjpre  29202  ch0le  29224  chle0  29226  chslej  29281  chjcom  29289  chub1  29290  chlub  29292  chlej1  29293  chlej2  29294  spansnsh  29344  fh1  29401  fh2  29402  chscllem1  29420  chscllem2  29421  chscllem3  29422  chscllem4  29423  chscl  29424  pjorthi  29452  pjoi0  29500  hstoc  30005  hstnmoc  30006  ch1dle  30135  atomli  30165  chirredlem3  30175  sumdmdii  30198