Metamath Proof Explorer


Theorem pjfoi

Description: A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis pjfn.1
|- H e. CH
Assertion pjfoi
|- ( projh ` H ) : ~H -onto-> H

Proof

Step Hyp Ref Expression
1 pjfn.1
 |-  H e. CH
2 1 pjfni
 |-  ( projh ` H ) Fn ~H
3 1 pjrni
 |-  ran ( projh ` H ) = H
4 df-fo
 |-  ( ( projh ` H ) : ~H -onto-> H <-> ( ( projh ` H ) Fn ~H /\ ran ( projh ` H ) = H ) )
5 2 3 4 mpbir2an
 |-  ( projh ` H ) : ~H -onto-> H