Metamath Proof Explorer

Theorem pjfn

Description: Functionality of a projection. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion pjfn 
|- ( H e. CH -> ( projh ` H ) Fn ~H )

Proof

Step Hyp Ref Expression
1 pjhf 
 |-  ( H e. CH -> ( projh ` H ) : ~H --> ~H )
2 1 ffnd 
 |-  ( H e. CH -> ( projh ` H ) Fn ~H )