Theorem pjval

Description: Value of the projection map. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjfval2.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
	pjfval2.p	⊢ 𝑃 = ( proj1 ‘ 𝑊 )
	pjfval2.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
Assertion	pjval	⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑇 ) = ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjfval2.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
2		pjfval2.p	⊢ 𝑃 = ( proj1 ‘ 𝑊 )
3		pjfval2.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
4		id	⊢ ( 𝑥 = 𝑇 → 𝑥 = 𝑇 )
5		fveq2	⊢ ( 𝑥 = 𝑇 → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ 𝑇 ) )
6	4 5	oveq12d	⊢ ( 𝑥 = 𝑇 → ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) = ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) )
7	1 2 3	pjfval2	⊢ 𝐾 = ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) )
8		ovex	⊢ ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) ∈ V
9	6 7 8	fvmpt	⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑇 ) = ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) )