Theorem offn

Description: The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	offval.1	$$⊢\phi \to FFnA$$
	offval.2	$$⊢\phi \to GFnB$$
	offval.3	$$⊢\phi \to A\in V$$
	offval.4	$$⊢\phi \to B\in W$$
	offval.5	$$⊢A\cap B=S$$
Assertion	offn	$$⊢\phi \to \left(F{R}_{f}G\right)FnS$$

Proof

Step	Hyp	Ref	Expression
1		offval.1	$$⊢\phi \to FFnA$$
2		offval.2	$$⊢\phi \to GFnB$$
3		offval.3	$$⊢\phi \to A\in V$$
4		offval.4	$$⊢\phi \to B\in W$$
5		offval.5	$$⊢A\cap B=S$$
6		ovex	$$⊢F\left(x\right)RG\left(x\right)\in \mathrm{V}$$
7		eqid	$$⊢\left(x\in S⟼F\left(x\right)RG\left(x\right)\right)=\left(x\in S⟼F\left(x\right)RG\left(x\right)\right)$$
8	6 7	fnmpti	$$⊢\left(x\in S⟼F\left(x\right)RG\left(x\right)\right)FnS$$
9		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
10		eqidd	$$⊢\left(\phi \wedge x\in B\right)\to G\left(x\right)=G\left(x\right)$$
11	1 2 3 4 5 9 10	offval	$$⊢\phi \to F{R}_{f}G=\left(x\in S⟼F\left(x\right)RG\left(x\right)\right)$$
12	11	fneq1d	$$⊢\phi \to \left(\left(F{R}_{f}G\right)FnS\leftrightarrow \left(x\in S⟼F\left(x\right)RG\left(x\right)\right)FnS\right)$$
13	8 12	mpbiri	$$⊢\phi \to \left(F{R}_{f}G\right)FnS$$