MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-css Structured version   Unicode version

Definition df-css 18224
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
StepHypRef Expression
1 ccss 18221 . 2  class  CSubSp
2 vh . . 3  setvar  h
3 cvv 3078 . . 3  class  _V
4 vs . . . . . 6  setvar  s
54cv 1369 . . . . 5  class  s
62cv 1369 . . . . . . . 8  class  h
7 cocv 18220 . . . . . . . 8  class  ocv
86, 7cfv 5529 . . . . . . 7  class  ( ocv `  h )
95, 8cfv 5529 . . . . . 6  class  ( ( ocv `  h ) `
 s )
109, 8cfv 5529 . . . . 5  class  ( ( ocv `  h ) `
 ( ( ocv `  h ) `  s
) )
115, 10wceq 1370 . . . 4  wff  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) )
1211, 4cab 2439 . . 3  class  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) }
132, 3, 12cmpt 4461 . 2  class  ( h  e.  _V  |->  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) } )
141, 13wceq 1370 1  wff  CSubSp  =  ( h  e.  _V  |->  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  cssval  18242
  Copyright terms: Public domain W3C validator