Theorem pjhf

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

	Ref	Expression
Assertion	pjhf	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ )

Proof

Step	Hyp	Ref	Expression
1		pjhfo	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 )
2		fof	⊢ ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 → ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 )
3	1 2	syl	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 )
4		chss	⊢ ( 𝐻 ∈ Cℋ → 𝐻 ⊆ ℋ )
5	3 4	fssd	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ )