Theorem ofcfval4

Description: The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval4.1	$$⊢\phi \to F:A⟶B$$
	ofcfval4.2	$$⊢\phi \to A\in V$$
	ofcfval4.3	$$⊢\phi \to C\in W$$
Assertion	ofcfval4	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(x\in B⟼xRC\right)\circ F$$

Proof

Step	Hyp	Ref	Expression
1		ofcfval4.1	$$⊢\phi \to F:A⟶B$$
2		ofcfval4.2	$$⊢\phi \to A\in V$$
3		ofcfval4.3	$$⊢\phi \to C\in W$$
4	1	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
5	4	mpteq1d	$$⊢\phi \to \left(y\in \mathrm{dom}F⟼F\left(y\right)RC\right)=\left(y\in A⟼F\left(y\right)RC\right)$$
6		fex	$$⊢\left(F:A⟶B\wedge A\in V\right)\to F\in \mathrm{V}$$
7	1 2 6	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
8		ofcfval3	$$⊢\left(F\in \mathrm{V}\wedge C\in W\right)\to F{\circ }_{\mathrm{fc}}RC=\left(y\in \mathrm{dom}F⟼F\left(y\right)RC\right)$$
9	7 3 8	syl2anc	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(y\in \mathrm{dom}F⟼F\left(y\right)RC\right)$$
10	1	ffvelrnda	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in B$$
11	1	feqmptd	$$⊢\phi \to F=\left(y\in A⟼F\left(y\right)\right)$$
12		eqidd	$$⊢\phi \to \left(x\in B⟼xRC\right)=\left(x\in B⟼xRC\right)$$
13		oveq1	$$⊢x=F\left(y\right)\to xRC=F\left(y\right)RC$$
14	10 11 12 13	fmptco	$$⊢\phi \to \left(x\in B⟼xRC\right)\circ F=\left(y\in A⟼F\left(y\right)RC\right)$$
15	5 9 14	3eqtr4d	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(x\in B⟼xRC\right)\circ F$$