Theorem ofval

Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-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$$
	ofval.6	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)=C$$
	ofval.7	$$⊢\left(\phi \wedge X\in B\right)\to G\left(X\right)=D$$
Assertion	ofval	$$⊢\left(\phi \wedge X\in S\right)\to \left(F{R}_{f}G\right)\left(X\right)=CRD$$

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		ofval.6	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)=C$$
7		ofval.7	$$⊢\left(\phi \wedge X\in B\right)\to G\left(X\right)=D$$
8		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
9		eqidd	$$⊢\left(\phi \wedge x\in B\right)\to G\left(x\right)=G\left(x\right)$$
10	1 2 3 4 5 8 9	offval	$$⊢\phi \to F{R}_{f}G=\left(x\in S⟼F\left(x\right)RG\left(x\right)\right)$$
11	10	fveq1d	$$⊢\phi \to \left(F{R}_{f}G\right)\left(X\right)=\left(x\in S⟼F\left(x\right)RG\left(x\right)\right)\left(X\right)$$
12	11	adantr	$$⊢\left(\phi \wedge X\in S\right)\to \left(F{R}_{f}G\right)\left(X\right)=\left(x\in S⟼F\left(x\right)RG\left(x\right)\right)\left(X\right)$$
13		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
14		fveq2	$$⊢x=X\to G\left(x\right)=G\left(X\right)$$
15	13 14	oveq12d	$$⊢x=X\to F\left(x\right)RG\left(x\right)=F\left(X\right)RG\left(X\right)$$
16		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)$$
17		ovex	$$⊢F\left(X\right)RG\left(X\right)\in \mathrm{V}$$
18	15 16 17	fvmpt	$$⊢X\in S\to \left(x\in S⟼F\left(x\right)RG\left(x\right)\right)\left(X\right)=F\left(X\right)RG\left(X\right)$$
19	18	adantl	$$⊢\left(\phi \wedge X\in S\right)\to \left(x\in S⟼F\left(x\right)RG\left(x\right)\right)\left(X\right)=F\left(X\right)RG\left(X\right)$$
20		inss1	$$⊢A\cap B\subseteq A$$
21	5 20	eqsstrri	$$⊢S\subseteq A$$
22	21	sseli	$$⊢X\in S\to X\in A$$
23	22 6	sylan2	$$⊢\left(\phi \wedge X\in S\right)\to F\left(X\right)=C$$
24		inss2	$$⊢A\cap B\subseteq B$$
25	5 24	eqsstrri	$$⊢S\subseteq B$$
26	25	sseli	$$⊢X\in S\to X\in B$$
27	26 7	sylan2	$$⊢\left(\phi \wedge X\in S\right)\to G\left(X\right)=D$$
28	23 27	oveq12d	$$⊢\left(\phi \wedge X\in S\right)\to F\left(X\right)RG\left(X\right)=CRD$$
29	12 19 28	3eqtrd	$$⊢\left(\phi \wedge X\in S\right)\to \left(F{R}_{f}G\right)\left(X\right)=CRD$$