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

Definition df-css 16580
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 16577 . 2  class  CSubSp
2 vh . . 3  set  h
3 cvv 2801 . . 3  class  _V
4 vs . . . . . 6  set  s
54cv 1631 . . . . 5  class  s
62cv 1631 . . . . . . . 8  class  h
7 cocv 16576 . . . . . . . 8  class  ocv
86, 7cfv 5271 . . . . . . 7  class  ( ocv `  h )
95, 8cfv 5271 . . . . . 6  class  ( ( ocv `  h ) `
 s )
109, 8cfv 5271 . . . . 5  class  ( ( ocv `  h ) `
 ( ( ocv `  h ) `  s
) )
115, 10wceq 1632 . . . 4  wff  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) )
1211, 4cab 2282 . . 3  class  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) }
132, 3, 12cmpt 4093 . 2  class  ( h  e.  _V  |->  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) } )
141, 13wceq 1632 1  wff  CSubSp  =  ( h  e.  _V  |->  { s  |  s  =  ( ( ocv `  h
) `  ( ( ocv `  h ) `  s ) ) } )
Colors of variables: wff set class
This definition is referenced by:  cssval  16598
  Copyright terms: Public domain W3C validator