Theorem chsh 29586

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3887   “ cima 5592  (class class class)co 7275   ↑_m cmap 8615  ℕcn 11973   ⇝_𝑣 chli 29289   S_ℋ csh 29290   C_ℋ cch 29291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fv 6441  df-ov 7278  df-ch 29583

This theorem is referenced by:  chsssh  29587  chshii  29589  ch0  29590  chss  29591  choccl  29668  chjval  29714  chjcl  29719  pjhth  29755  pjhtheu  29756  pjpreeq  29760  pjpjpre  29781  ch0le  29803  chle0  29805  chslej  29860  chjcom  29868  chub1  29869  chlub  29871  chlej1  29872  chlej2  29873  spansnsh  29923  fh1  29980  fh2  29981  chscllem1  29999  chscllem2  30000  chscllem3  30001  chscllem4  30002  chscl  30003  pjorthi  30031  pjoi0  30079  hstoc  30584  hstnmoc  30585  ch1dle  30714  atomli  30744  chirredlem3  30754  sumdmdii  30777