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

Definition df-thl 19828
 Description: Define the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.)
Assertion
Ref Expression
df-thl toHL = ( ∈ V ↦ ((toInc‘(CSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))

Detailed syntax breakdown of Definition df-thl
StepHypRef Expression
1 cthl 19825 . 2 class toHL
2 vh . . 3 setvar
3 cvv 3173 . . 3 class V
42cv 1474 . . . . . 6 class
5 ccss 19824 . . . . . 6 class CSubSp
64, 5cfv 5804 . . . . 5 class (CSubSp‘)
7 cipo 16974 . . . . 5 class toInc
86, 7cfv 5804 . . . 4 class (toInc‘(CSubSp‘))
9 cnx 15692 . . . . . 6 class ndx
10 coc 15776 . . . . . 6 class oc
119, 10cfv 5804 . . . . 5 class (oc‘ndx)
12 cocv 19823 . . . . . 6 class ocv
134, 12cfv 5804 . . . . 5 class (ocv‘)
1411, 13cop 4131 . . . 4 class ⟨(oc‘ndx), (ocv‘)⟩
15 csts 15693 . . . 4 class sSet
168, 14, 15co 6549 . . 3 class ((toInc‘(CSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩)
172, 3, 16cmpt 4643 . 2 class ( ∈ V ↦ ((toInc‘(CSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
181, 17wceq 1475 1 wff toHL = ( ∈ V ↦ ((toInc‘(CSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
 Colors of variables: wff setvar class This definition is referenced by:  thlval  19858
 Copyright terms: Public domain W3C validator