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	⊢ ClSubSp = ( ℎ ∈ V ↦ { 𝑠 ∣ 𝑠 = ( ( ocv ‘ ℎ ) ‘ ( ( ocv ‘ ℎ ) ‘ 𝑠 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccss	⊢ ClSubSp
1		vh	⊢ ℎ
2		cvv	⊢ V
3		vs	⊢ 𝑠
4	3	cv	⊢ 𝑠
5		cocv	⊢ ocv
6	1	cv	⊢ ℎ
7	6 5	cfv	⊢ ( ocv ‘ ℎ )
8	4 7	cfv	⊢ ( ( ocv ‘ ℎ ) ‘ 𝑠 )
9	8 7	cfv	⊢ ( ( ocv ‘ ℎ ) ‘ ( ( ocv ‘ ℎ ) ‘ 𝑠 ) )
10	4 9	wceq	⊢ 𝑠 = ( ( ocv ‘ ℎ ) ‘ ( ( ocv ‘ ℎ ) ‘ 𝑠 ) )
11	10 3	cab	⊢ { 𝑠 ∣ 𝑠 = ( ( ocv ‘ ℎ ) ‘ ( ( ocv ‘ ℎ ) ‘ 𝑠 ) ) }
12	1 2 11	cmpt	⊢ ( ℎ ∈ V ↦ { 𝑠 ∣ 𝑠 = ( ( ocv ‘ ℎ ) ‘ ( ( ocv ‘ ℎ ) ‘ 𝑠 ) ) } )
13	0 12	wceq	⊢ ClSubSp = ( ℎ ∈ V ↦ { 𝑠 ∣ 𝑠 = ( ( ocv ‘ ℎ ) ‘ ( ( ocv ‘ ℎ ) ‘ 𝑠 ) ) } )