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

Definition df-thl 19928
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 19925 . 2 class toHL
2 vh . . 3 setvar
3 cvv 3186 . . 3 class V
42cv 1479 . . . . . 6 class
5 ccss 19924 . . . . . 6 class CSubSp
64, 5cfv 5847 . . . . 5 class (CSubSp‘)
7 cipo 17072 . . . . 5 class toInc
86, 7cfv 5847 . . . 4 class (toInc‘(CSubSp‘))
9 cnx 15778 . . . . . 6 class ndx
10 coc 15870 . . . . . 6 class oc
119, 10cfv 5847 . . . . 5 class (oc‘ndx)
12 cocv 19923 . . . . . 6 class ocv
134, 12cfv 5847 . . . . 5 class (ocv‘)
1411, 13cop 4154 . . . 4 class ⟨(oc‘ndx), (ocv‘)⟩
15 csts 15779 . . . 4 class sSet
168, 14, 15co 6604 . . 3 class ((toInc‘(CSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩)
172, 3, 16cmpt 4673 . 2 class ( ∈ V ↦ ((toInc‘(CSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
181, 17wceq 1480 1 wff toHL = ( ∈ V ↦ ((toInc‘(CSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  thlval  19958
  Copyright terms: Public domain W3C validator