Theorem pjval

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

	Ref	Expression
Hypotheses	pjfval2.o	|- ._|_ = ( ocv ` W )
	pjfval2.p	|- P = ( proj1 ` W )
	pjfval2.k	|- K = ( proj ` W )
Assertion	pjval	|- ( T e. dom K -> ( K ` T ) = ( T P ( ._|_ ` T ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjfval2.o	|- ._|_ = ( ocv ` W )
2		pjfval2.p	|- P = ( proj1 ` W )
3		pjfval2.k	|- K = ( proj ` W )
4		id	|- ( x = T -> x = T )
5		fveq2	|- ( x = T -> ( ._|_ ` x ) = ( ._|_ ` T ) )
6	4 5	oveq12d	|- ( x = T -> ( x P ( ._|_ ` x ) ) = ( T P ( ._|_ ` T ) ) )
7	1 2 3	pjfval2	|- K = ( x e. dom K |-> ( x P ( ._|_ ` x ) ) )
8		ovex	|- ( T P ( ._|_ ` T ) ) e. _V
9	6 7 8	fvmpt	|- ( T e. dom K -> ( K ` T ) = ( T P ( ._|_ ` T ) ) )