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

Definition df-thl 16581
Description: Define the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.)
Assertion
Ref Expression
df-thl  |- toHL  =  ( h  e.  _V  |->  ( (toInc `  ( CSubSp `  h ) ) sSet  <. ( oc `  ndx ) ,  ( ocv `  h
) >. ) )

Detailed syntax breakdown of Definition df-thl
StepHypRef Expression
1 cthl 16578 . 2  class toHL
2 vh . . 3  set  h
3 cvv 2801 . . 3  class  _V
42cv 1631 . . . . . 6  class  h
5 ccss 16577 . . . . . 6  class  CSubSp
64, 5cfv 5271 . . . . 5  class  ( CSubSp `  h )
7 cipo 14270 . . . . 5  class toInc
86, 7cfv 5271 . . . 4  class  (toInc `  ( CSubSp `  h )
)
9 cnx 13161 . . . . . 6  class  ndx
10 coc 13232 . . . . . 6  class  oc
119, 10cfv 5271 . . . . 5  class  ( oc
`  ndx )
12 cocv 16576 . . . . . 6  class  ocv
134, 12cfv 5271 . . . . 5  class  ( ocv `  h )
1411, 13cop 3656 . . . 4  class  <. ( oc `  ndx ) ,  ( ocv `  h
) >.
15 csts 13162 . . . 4  class sSet
168, 14, 15co 5874 . . 3  class  ( (toInc `  ( CSubSp `  h )
) sSet  <. ( oc `  ndx ) ,  ( ocv `  h ) >. )
172, 3, 16cmpt 4093 . 2  class  ( h  e.  _V  |->  ( (toInc `  ( CSubSp `  h )
) sSet  <. ( oc `  ndx ) ,  ( ocv `  h ) >. )
)
181, 17wceq 1632 1  wff toHL  =  ( h  e.  _V  |->  ( (toInc `  ( CSubSp `  h ) ) sSet  <. ( oc `  ndx ) ,  ( ocv `  h
) >. ) )
Colors of variables: wff set class
This definition is referenced by:  thlval  16611
  Copyright terms: Public domain W3C validator