Theorem ofcfn

Description: The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval.1	$$⊢\phi \to FFnA$$
	ofcfval.2	$$⊢\phi \to A\in V$$
	ofcfval.3	$$⊢\phi \to C\in W$$
Assertion	ofcfn	$$⊢\phi \to \left(F{\circ }_{\mathrm{fc}}RC\right)FnA$$

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	$$⊢\phi \to FFnA$$
2		ofcfval.2	$$⊢\phi \to A\in V$$
3		ofcfval.3	$$⊢\phi \to C\in W$$
4		ovex	$$⊢F\left(x\right)RC\in \mathrm{V}$$
5		eqid	$$⊢\left(x\in A⟼F\left(x\right)RC\right)=\left(x\in A⟼F\left(x\right)RC\right)$$
6	4 5	fnmpti	$$⊢\left(x\in A⟼F\left(x\right)RC\right)FnA$$
7		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
8	1 2 3 7	ofcfval	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(x\in A⟼F\left(x\right)RC\right)$$
9	8	fneq1d	$$⊢\phi \to \left(\left(F{\circ }_{\mathrm{fc}}RC\right)FnA\leftrightarrow \left(x\in A⟼F\left(x\right)RC\right)FnA\right)$$
10	6 9	mpbiri	$$⊢\phi \to \left(F{\circ }_{\mathrm{fc}}RC\right)FnA$$