Theorem pjmfn

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

	Ref	Expression
Assertion	pjmfn	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2	1	mptex	$$⊢\left(x\in \mathscr{H}⟼\left(\iota z\in h|\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y\right)\right)\in \mathrm{V}$$
3		df-pjh	$$⊢{\mathrm{proj}}_{ℎ}=\left(h\in {\mathbf{C}}_{\mathscr{H}}⟼\left(x\in \mathscr{H}⟼\left(\iota z\in h|\exists y\in \perp \left(h\right)x=z{+}_{ℎ}y\right)\right)\right)$$
4	2 3	fnmpti	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}$$