Theorem pjmfn

Description: Functionality of the projection function. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjmfn	⊢ projℎ Fn Cℋ

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	⊢ ℋ ∈ V
2	1	mptex	⊢ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) ∈ V
3		df-pjh	⊢ projℎ = ( ℎ ∈ Cℋ ↦ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) )
4	2 3	fnmpti	⊢ projℎ Fn Cℋ