Metamath Proof Explorer

Theorem pjrn

Description: The range of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjrn 
|- ( H e. CH -> ran ( projh ` H ) = H )

Proof

Step Hyp Ref Expression
1 pjhfo 
 |-  ( H e. CH -> ( projh ` H ) : ~H -onto-> H )
2 forn 
 |-  ( ( projh ` H ) : ~H -onto-> H -> ran ( projh ` H ) = H )
3 1 2 syl 
 |-  ( H e. CH -> ran ( projh ` H ) = H )