Definition df-css 21970

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

Assertion

Ref	Expression
df-css	⊢ ClSubSp = (ℎ ∈ V ↦ {𝑠 ∣ 𝑠 = ((ocv‘ℎ)‘((ocv‘ℎ)‘𝑠))})

Distinct variable group:   ℎ,𝑠

Detailed syntax breakdown of Definition df-css

Step	Hyp	Ref	Expression
1		ccss 21967	. 2 class ClSubSp
2		vh	. . 3 setvar ℎ
3		cvv 3450	. . 3 class V
4		vs	. . . . . 6 setvar 𝑠
5	4	cv 1568	. . . . 5 class 𝑠
6	2	cv 1568	. . . . . . . 8 class ℎ
7		cocv 21966	. . . . . . . 8 class ocv
8	6, 7	cfv 6538	. . . . . . 7 class (ocv‘ℎ)
9	5, 8	cfv 6538	. . . . . 6 class ((ocv‘ℎ)‘𝑠)
10	9, 8	cfv 6538	. . . . 5 class ((ocv‘ℎ)‘((ocv‘ℎ)‘𝑠))
11	5, 10	wceq 1569	. . . 4 wff 𝑠 = ((ocv‘ℎ)‘((ocv‘ℎ)‘𝑠))
12	11, 4	cab 2738	. . 3 class {𝑠 ∣ 𝑠 = ((ocv‘ℎ)‘((ocv‘ℎ)‘𝑠))}
13	2, 3, 12	cmpt 5185	. 2 class (ℎ ∈ V ↦ {𝑠 ∣ 𝑠 = ((ocv‘ℎ)‘((ocv‘ℎ)‘𝑠))})
14	1, 13	wceq 1569	1 wff ClSubSp = (ℎ ∈ V ↦ {𝑠 ∣ 𝑠 = ((ocv‘ℎ)‘((ocv‘ℎ)‘𝑠))})

This definition is used by:  cssval  21988