This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) , ⊥ ⟩ ) )