Definition df-css 20008

Description: Define set of closed subspaces. (Contributed by NM, 7-Oct-2011.)

Assertion

Ref	Expression
df-css	|- CSubSp = ( h e. _V |-> { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) } )

Distinct variable group:   h, s

Detailed syntax breakdown of Definition df-css

Step	Hyp	Ref	Expression
1		ccss 20005	. 2 class CSubSp
2		vh	. . 3 setvar h
3		cvv 3200	. . 3 class _V
4		vs	. . . . . 6 setvar s
5	4	cv 1482	. . . . 5 class s
6	2	cv 1482	. . . . . . . 8 class h
7		cocv 20004	. . . . . . . 8 class ocv
8	6, 7	cfv 5888	. . . . . . 7 class ( ocv ` h )
9	5, 8	cfv 5888	. . . . . 6 class ( ( ocv ` h ) ` s )
10	9, 8	cfv 5888	. . . . 5 class ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) )
11	5, 10	wceq 1483	. . . 4 wff s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) )
12	11, 4	cab 2608	. . 3 class { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) }
13	2, 3, 12	cmpt 4729	. 2 class ( h e. _V |-> { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) } )
14	1, 13	wceq 1483	1 wff CSubSp = ( h e. _V |-> { s | s = ( ( ocv ` h ) ` ( ( ocv ` h ) ` s ) ) } )

This definition is referenced by:  cssval  20026