Description: Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | shsspwh | ⊢ Sℋ ⊆ 𝒫 ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwuni | ⊢ Sℋ ⊆ 𝒫 ∪ Sℋ | |
2 | helsh | ⊢ ℋ ∈ Sℋ | |
3 | shss | ⊢ ( 𝑥 ∈ Sℋ → 𝑥 ⊆ ℋ ) | |
4 | 3 | rgen | ⊢ ∀ 𝑥 ∈ Sℋ 𝑥 ⊆ ℋ |
5 | ssunieq | ⊢ ( ( ℋ ∈ Sℋ ∧ ∀ 𝑥 ∈ Sℋ 𝑥 ⊆ ℋ ) → ℋ = ∪ Sℋ ) | |
6 | 2 4 5 | mp2an | ⊢ ℋ = ∪ Sℋ |
7 | 6 | pweqi | ⊢ 𝒫 ℋ = 𝒫 ∪ Sℋ |
8 | 1 7 | sseqtrri | ⊢ Sℋ ⊆ 𝒫 ℋ |