Theorem chsh 31253

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3963   “ cima 5692  (class class class)co 7431   ↑_m cmap 8865  ℕcn 12264   ⇝_𝑣 chli 30956   S_ℋ csh 30957   C_ℋ cch 30958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fv 6571  df-ov 7434  df-ch 31250

This theorem is referenced by:  chsssh  31254  chshii  31256  ch0  31257  chss  31258  choccl  31335  chjval  31381  chjcl  31386  pjhth  31422  pjhtheu  31423  pjpreeq  31427  pjpjpre  31448  ch0le  31470  chle0  31472  chslej  31527  chjcom  31535  chub1  31536  chlub  31538  chlej1  31539  chlej2  31540  spansnsh  31590  fh1  31647  fh2  31648  chscllem1  31666  chscllem2  31667  chscllem3  31668  chscllem4  31669  chscl  31670  pjorthi  31698  pjoi0  31746  hstoc  32251  hstnmoc  32252  ch1dle  32381  atomli  32411  chirredlem3  32421  sumdmdii  32444