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

Definition df-css 18885
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 18882 . 2  class  CSubSp
2 vh . . 3  setvar  h
3 cvv 3058 . . 3  class  _V
4 vs . . . . . 6  setvar  s
54cv 1404 . . . . 5  class  s
62cv 1404 . . . . . . . 8  class  h
7 cocv 18881 . . . . . . . 8  class  ocv
86, 7cfv 5525 . . . . . . 7  class  ( ocv `  h )
95, 8cfv 5525 . . . . . 6  class  ( ( ocv `  h ) `
 s )
109, 8cfv 5525 . . . . 5  class  ( ( ocv `  h ) `
 ( ( ocv `  h ) `  s
) )
115, 10wceq 1405 . . . 4  wff  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) )
1211, 4cab 2387 . . 3  class  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) }
132, 3, 12cmpt 4452 . 2  class  ( h  e.  _V  |->  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) } )
141, 13wceq 1405 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  18903
  Copyright terms: Public domain W3C validator