# Metamath Proof Explorer

## Theorem thlval

Description: Value of the Hilbert lattice. (Contributed by Mario Carneiro, 25-Oct-2015)

Ref Expression
Hypotheses thlval.k ${⊢}{K}=\mathrm{toHL}\left({W}\right)$
thlval.c ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
thlval.i ${⊢}{I}=\mathrm{toInc}\left({C}\right)$
thlval.o
Assertion thlval

### Proof

Step Hyp Ref Expression
1 thlval.k ${⊢}{K}=\mathrm{toHL}\left({W}\right)$
2 thlval.c ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
3 thlval.i ${⊢}{I}=\mathrm{toInc}\left({C}\right)$
4 thlval.o
5 elex ${⊢}{W}\in {V}\to {W}\in \mathrm{V}$
6 fveq2 ${⊢}{h}={W}\to \mathrm{ClSubSp}\left({h}\right)=\mathrm{ClSubSp}\left({W}\right)$
7 6 2 eqtr4di ${⊢}{h}={W}\to \mathrm{ClSubSp}\left({h}\right)={C}$
8 7 fveq2d ${⊢}{h}={W}\to \mathrm{toInc}\left(\mathrm{ClSubSp}\left({h}\right)\right)=\mathrm{toInc}\left({C}\right)$
9 8 3 eqtr4di ${⊢}{h}={W}\to \mathrm{toInc}\left(\mathrm{ClSubSp}\left({h}\right)\right)={I}$
10 fveq2 ${⊢}{h}={W}\to \mathrm{ocv}\left({h}\right)=\mathrm{ocv}\left({W}\right)$
11 10 4 eqtr4di
12 11 opeq2d
13 9 12 oveq12d
14 df-thl ${⊢}\mathrm{toHL}=\left({h}\in \mathrm{V}⟼\mathrm{toInc}\left(\mathrm{ClSubSp}\left({h}\right)\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left({h}\right)⟩\right)$
15 ovex
16 13 14 15 fvmpt
17 1 16 syl5eq
18 5 17 syl