Metamath Proof Explorer

Theorem thlval

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

Ref Expression
Hypotheses thlval.k ⊢K=toHL⁡W
thlval.c ⊢C=ClSubSp⁡W
thlval.i ⊢I=toInc⁡C
thlval.o ⊢⊥˙=ocv⁡W
Assertion thlval ⊢W∈V→K=IsSetoc⁡ndx⊥˙

Proof

Step Hyp Ref Expression
1 thlval.k ⊢K=toHL⁡W
2 thlval.c ⊢C=ClSubSp⁡W
3 thlval.i ⊢I=toInc⁡C
4 thlval.o ⊢⊥˙=ocv⁡W
5 elex ⊢W∈V→W∈V
6 fveq2 ⊢h=W→ClSubSp⁡h=ClSubSp⁡W
7 6 2 eqtr4di ⊢h=W→ClSubSp⁡h=C
8 7 fveq2d ⊢h=W→toInc⁡ClSubSp⁡h=toInc⁡C
9 8 3 eqtr4di ⊢h=W→toInc⁡ClSubSp⁡h=I
10 fveq2 ⊢h=W→ocv⁡h=ocv⁡W
11 10 4 eqtr4di ⊢h=W→ocv⁡h=⊥˙
12 11 opeq2d ⊢h=W→oc⁡ndxocv⁡h=oc⁡ndx⊥˙
13 9 12 oveq12d ⊢h=W→toInc⁡ClSubSp⁡hsSetoc⁡ndxocv⁡h=IsSetoc⁡ndx⊥˙
14 df-thl ⊢toHL=h∈V⟼toInc⁡ClSubSp⁡hsSetoc⁡ndxocv⁡h
15 ovex ⊢IsSetoc⁡ndx⊥˙∈V
16 13 14 15 fvmpt ⊢W∈V→toHL⁡W=IsSetoc⁡ndx⊥˙
17 1 16 eqtrid ⊢W∈V→K=IsSetoc⁡ndx⊥˙
18 5 17 syl ⊢W∈V→K=IsSetoc⁡ndx⊥˙