Theorem pjmfn

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

	Ref	Expression
Assertion	pjmfn	|- projh Fn CH

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	|- ~H e. _V
2	1	mptex	|- ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) e. _V
3		df-pjh	|- projh = ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )
4	2 3	fnmpti	|- projh Fn CH