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 = I sSet oc ⁡ 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 ⁡ ndx ocv ⁡ h = oc ⁡ ndx ⊥ ˙
13 9 12 oveq12d ⊢ h = W → toInc ⁡ ClSubSp ⁡ h sSet oc ⁡ ndx ocv ⁡ h = I sSet oc ⁡ ndx ⊥ ˙
14 df-thl ⊢ toHL = h ∈ V ⟼ toInc ⁡ ClSubSp ⁡ h sSet oc ⁡ ndx ocv ⁡ h
15 ovex ⊢ I sSet oc ⁡ ndx ⊥ ˙ ∈ V
16 13 14 15 fvmpt ⊢ W ∈ V → toHL ⁡ W = I sSet oc ⁡ ndx ⊥ ˙
17 1 16 syl5eq ⊢ W ∈ V → K = I sSet oc ⁡ ndx ⊥ ˙
18 5 17 syl ⊢ W ∈ V → K = I sSet oc ⁡ ndx ⊥ ˙