Theorem pjfn

Description: Functionality of a projection. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjfn	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) Fn ℋ )

Proof

Step	Hyp	Ref	Expression
1		pjhf	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ )
2	1	ffnd	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) Fn ℋ )