Theorem pjfni

Description: Functionality of a projection. (Contributed by NM, 30-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjfn.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjfni	⊢ ( projℎ ‘ 𝐻 ) Fn ℋ

Proof

Step	Hyp	Ref	Expression
1		pjfn.1	⊢ 𝐻 ∈ Cℋ
2		riotaex	⊢ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∈ V
3		pjhfval	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) = ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ) )
4	1 3	ax-mp	⊢ ( projℎ ‘ 𝐻 ) = ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) )
5	2 4	fnmpti	⊢ ( projℎ ‘ 𝐻 ) Fn ℋ