Metamath Proof Explorer


Theorem pjval

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

Ref Expression
Hypotheses pjfval2.o ˙=ocvW
pjfval2.p P=proj1W
pjfval2.k K=projW
Assertion pjval TdomKKT=TP˙T

Proof

Step Hyp Ref Expression
1 pjfval2.o ˙=ocvW
2 pjfval2.p P=proj1W
3 pjfval2.k K=projW
4 id x=Tx=T
5 fveq2 x=T˙x=˙T
6 4 5 oveq12d x=TxP˙x=TP˙T
7 1 2 3 pjfval2 K=xdomKxP˙x
8 ovex TP˙TV
9 6 7 8 fvmpt TdomKKT=TP˙T