Theorem chsh 31126

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911   “ cima 5634  (class class class)co 7369   ↑_m cmap 8776  ℕcn 12162   ⇝_𝑣 chli 30829   S_ℋ csh 30830   C_ℋ cch 30831

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fv 6507  df-ov 7372  df-ch 31123

This theorem is referenced by:  chsssh  31127  chshii  31129  ch0  31130  chss  31131  choccl  31208  chjval  31254  chjcl  31259  pjhth  31295  pjhtheu  31296  pjpreeq  31300  pjpjpre  31321  ch0le  31343  chle0  31345  chslej  31400  chjcom  31408  chub1  31409  chlub  31411  chlej1  31412  chlej2  31413  spansnsh  31463  fh1  31520  fh2  31521  chscllem1  31539  chscllem2  31540  chscllem3  31541  chscllem4  31542  chscl  31543  pjorthi  31571  pjoi0  31619  hstoc  32124  hstnmoc  32125  ch1dle  32254  atomli  32284  chirredlem3  32294  sumdmdii  32317