# Metamath Proof Explorer

## Definition df-css

Description: Define the set of closed (linear) subspaces of a given pre-Hilbert space. (Contributed by NM, 7-Oct-2011)

Ref Expression
Assertion df-css ${⊢}\mathrm{ClSubSp}=\left({h}\in \mathrm{V}⟼\left\{{s}|{s}=\mathrm{ocv}\left({h}\right)\left(\mathrm{ocv}\left({h}\right)\left({s}\right)\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccss ${class}\mathrm{ClSubSp}$
1 vh ${setvar}{h}$
2 cvv ${class}\mathrm{V}$
3 vs ${setvar}{s}$
4 3 cv ${setvar}{s}$
5 cocv ${class}\mathrm{ocv}$
6 1 cv ${setvar}{h}$
7 6 5 cfv ${class}\mathrm{ocv}\left({h}\right)$
8 4 7 cfv ${class}\mathrm{ocv}\left({h}\right)\left({s}\right)$
9 8 7 cfv ${class}\mathrm{ocv}\left({h}\right)\left(\mathrm{ocv}\left({h}\right)\left({s}\right)\right)$
10 4 9 wceq ${wff}{s}=\mathrm{ocv}\left({h}\right)\left(\mathrm{ocv}\left({h}\right)\left({s}\right)\right)$
11 10 3 cab ${class}\left\{{s}|{s}=\mathrm{ocv}\left({h}\right)\left(\mathrm{ocv}\left({h}\right)\left({s}\right)\right)\right\}$
12 1 2 11 cmpt ${class}\left({h}\in \mathrm{V}⟼\left\{{s}|{s}=\mathrm{ocv}\left({h}\right)\left(\mathrm{ocv}\left({h}\right)\left({s}\right)\right)\right\}\right)$
13 0 12 wceq ${wff}\mathrm{ClSubSp}=\left({h}\in \mathrm{V}⟼\left\{{s}|{s}=\mathrm{ocv}\left({h}\right)\left(\mathrm{ocv}\left({h}\right)\left({s}\right)\right)\right\}\right)$