Theorem pjfoi

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

	Ref	Expression
Hypothesis	pjfn.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjfoi	⊢ ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻

Proof

Step	Hyp	Ref	Expression
1		pjfn.1	⊢ 𝐻 ∈ Cℋ
2	1	pjfni	⊢ ( projℎ ‘ 𝐻 ) Fn ℋ
3	1	pjrni	⊢ ran ( projℎ ‘ 𝐻 ) = 𝐻
4		df-fo	⊢ ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) Fn ℋ ∧ ran ( projℎ ‘ 𝐻 ) = 𝐻 ) )
5	2 3 4	mpbir2an	⊢ ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻