Metamath Proof Explorer

Theorem pjhf

Description: The mapping of a projection. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjhf 
|- ( H e. CH -> ( projh ` H ) : ~H --> ~H )

Proof

Step Hyp Ref Expression
1 pjhfo 
 |-  ( H e. CH -> ( projh ` H ) : ~H -onto-> H )
2 fof 
 |-  ( ( projh ` H ) : ~H -onto-> H -> ( projh ` H ) : ~H --> H )
3 1 2 syl 
 |-  ( H e. CH -> ( projh ` H ) : ~H --> H )
4 chss 
 |-  ( H e. CH -> H C_ ~H )
5 3 4 fssd 
 |-  ( H e. CH -> ( projh ` H ) : ~H --> ~H )