Metamath Proof Explorer


Theorem pjmfn

Description: Functionality of the projection function. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjmfn projFnC

Proof

Step Hyp Ref Expression
1 ax-hilex V
2 1 mptex xιzh|yhx=z+yV
3 df-pjh proj=hCxιzh|yhx=z+y
4 2 3 fnmpti projFnC