Theorem chsh 30986

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

Syntax hints:   → wi 4   ∈ wcel 2098   ⊆ wss 3943   “ cima 5672  (class class class)co 7405   ↑_m cmap 8822  ℕcn 12216   ⇝_𝑣 chli 30689   S_ℋ csh 30690   C_ℋ cch 30691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-xp 5675  df-cnv 5677  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fv 6545  df-ov 7408  df-ch 30983

This theorem is referenced by:  chsssh  30987  chshii  30989  ch0  30990  chss  30991  choccl  31068  chjval  31114  chjcl  31119  pjhth  31155  pjhtheu  31156  pjpreeq  31160  pjpjpre  31181  ch0le  31203  chle0  31205  chslej  31260  chjcom  31268  chub1  31269  chlub  31271  chlej1  31272  chlej2  31273  spansnsh  31323  fh1  31380  fh2  31381  chscllem1  31399  chscllem2  31400  chscllem3  31401  chscllem4  31402  chscl  31403  pjorthi  31431  pjoi0  31479  hstoc  31984  hstnmoc  31985  ch1dle  32114  atomli  32144  chirredlem3  32154  sumdmdii  32177