Theorem thlval

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

	Ref	Expression
Hypotheses	thlval.k	⊢ 𝐾 = ( toHL ‘ 𝑊 )
	thlval.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
	thlval.i	⊢ 𝐼 = ( toInc ‘ 𝐶 )
	thlval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion	thlval	⊢ ( 𝑊 ∈ 𝑉 → 𝐾 = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ⊥ ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		thlval.k	⊢ 𝐾 = ( toHL ‘ 𝑊 )
2		thlval.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3		thlval.i	⊢ 𝐼 = ( toInc ‘ 𝐶 )
4		thlval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
5		elex	⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
6		fveq2	⊢ ( ℎ = 𝑊 → ( ClSubSp ‘ ℎ ) = ( ClSubSp ‘ 𝑊 ) )
7	6 2	eqtr4di	⊢ ( ℎ = 𝑊 → ( ClSubSp ‘ ℎ ) = 𝐶 )
8	7	fveq2d	⊢ ( ℎ = 𝑊 → ( toInc ‘ ( ClSubSp ‘ ℎ ) ) = ( toInc ‘ 𝐶 ) )
9	8 3	eqtr4di	⊢ ( ℎ = 𝑊 → ( toInc ‘ ( ClSubSp ‘ ℎ ) ) = 𝐼 )
10		fveq2	⊢ ( ℎ = 𝑊 → ( ocv ‘ ℎ ) = ( ocv ‘ 𝑊 ) )
11	10 4	eqtr4di	⊢ ( ℎ = 𝑊 → ( ocv ‘ ℎ ) = ⊥ )
12	11	opeq2d	⊢ ( ℎ = 𝑊 → ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩ = ⟨ ( oc ‘ ndx ) , ⊥ ⟩ )
13	9 12	oveq12d	⊢ ( ℎ = 𝑊 → ( ( toInc ‘ ( ClSubSp ‘ ℎ ) ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩ ) = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ⊥ ⟩ ) )
14		df-thl	⊢ toHL = ( ℎ ∈ V ↦ ( ( toInc ‘ ( ClSubSp ‘ ℎ ) ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩ ) )
15		ovex	⊢ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ⊥ ⟩ ) ∈ V
16	13 14 15	fvmpt	⊢ ( 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ⊥ ⟩ ) )
17	1 16	eqtrid	⊢ ( 𝑊 ∈ V → 𝐾 = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ⊥ ⟩ ) )
18	5 17	syl	⊢ ( 𝑊 ∈ 𝑉 → 𝐾 = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ⊥ ⟩ ) )