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	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjfni	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)Fn\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		pjfn.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		riotaex	$$⊢\left(\iota y\in H|\exists z\in \perp \left(H\right)x=y{+}_{ℎ}z\right)\in \mathrm{V}$$
3		pjhfval	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)=\left(x\in \mathscr{H}⟼\left(\iota y\in H|\exists z\in \perp \left(H\right)x=y{+}_{ℎ}z\right)\right)$$
4	1 3	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)=\left(x\in \mathscr{H}⟼\left(\iota y\in H|\exists z\in \perp \left(H\right)x=y{+}_{ℎ}z\right)\right)$$
5	2 4	fnmpti	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)Fn\mathscr{H}$$