Step |
Hyp |
Ref |
Expression |
1 |
|
cssval.o |
|- ._|_ = ( ocv ` W ) |
2 |
|
cssval.c |
|- C = ( ClSubSp ` W ) |
3 |
|
elex |
|- ( W e. X -> W e. _V ) |
4 |
|
fveq2 |
|- ( w = W -> ( ocv ` w ) = ( ocv ` W ) ) |
5 |
4 1
|
eqtr4di |
|- ( w = W -> ( ocv ` w ) = ._|_ ) |
6 |
5
|
fveq1d |
|- ( w = W -> ( ( ocv ` w ) ` s ) = ( ._|_ ` s ) ) |
7 |
5 6
|
fveq12d |
|- ( w = W -> ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) = ( ._|_ ` ( ._|_ ` s ) ) ) |
8 |
7
|
eqeq2d |
|- ( w = W -> ( s = ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) <-> s = ( ._|_ ` ( ._|_ ` s ) ) ) ) |
9 |
8
|
abbidv |
|- ( w = W -> { s | s = ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) } = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } ) |
10 |
|
df-css |
|- ClSubSp = ( w e. _V |-> { s | s = ( ( ocv ` w ) ` ( ( ocv ` w ) ` s ) ) } ) |
11 |
|
fvex |
|- ( Base ` W ) e. _V |
12 |
11
|
pwex |
|- ~P ( Base ` W ) e. _V |
13 |
|
id |
|- ( s = ( ._|_ ` ( ._|_ ` s ) ) -> s = ( ._|_ ` ( ._|_ ` s ) ) ) |
14 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
15 |
14 1
|
ocvss |
|- ( ._|_ ` ( ._|_ ` s ) ) C_ ( Base ` W ) |
16 |
|
fvex |
|- ( ._|_ ` ( ._|_ ` s ) ) e. _V |
17 |
16
|
elpw |
|- ( ( ._|_ ` ( ._|_ ` s ) ) e. ~P ( Base ` W ) <-> ( ._|_ ` ( ._|_ ` s ) ) C_ ( Base ` W ) ) |
18 |
15 17
|
mpbir |
|- ( ._|_ ` ( ._|_ ` s ) ) e. ~P ( Base ` W ) |
19 |
13 18
|
eqeltrdi |
|- ( s = ( ._|_ ` ( ._|_ ` s ) ) -> s e. ~P ( Base ` W ) ) |
20 |
19
|
abssi |
|- { s | s = ( ._|_ ` ( ._|_ ` s ) ) } C_ ~P ( Base ` W ) |
21 |
12 20
|
ssexi |
|- { s | s = ( ._|_ ` ( ._|_ ` s ) ) } e. _V |
22 |
9 10 21
|
fvmpt |
|- ( W e. _V -> ( ClSubSp ` W ) = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } ) |
23 |
2 22
|
syl5eq |
|- ( W e. _V -> C = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } ) |
24 |
3 23
|
syl |
|- ( W e. X -> C = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } ) |