Theorem chsh 31168

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903   “ cima 5622  (class class class)co 7349   ↑_m cmap 8753  ℕcn 12128   ⇝_𝑣 chli 30871   S_ℋ csh 30872   C_ℋ cch 30873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fv 6490  df-ov 7352  df-ch 31165

This theorem is referenced by:  chsssh  31169  chshii  31171  ch0  31172  chss  31173  choccl  31250  chjval  31296  chjcl  31301  pjhth  31337  pjhtheu  31338  pjpreeq  31342  pjpjpre  31363  ch0le  31385  chle0  31387  chslej  31442  chjcom  31450  chub1  31451  chlub  31453  chlej1  31454  chlej2  31455  spansnsh  31505  fh1  31562  fh2  31563  chscllem1  31581  chscllem2  31582  chscllem3  31583  chscllem4  31584  chscl  31585  pjorthi  31613  pjoi0  31661  hstoc  32166  hstnmoc  32167  ch1dle  32296  atomli  32326  chirredlem3  32336  sumdmdii  32359