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	1 2	fexd	$$⊢\phi \to F\in \mathrm{V}$$
7		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)$$
8	6 3 7	syl2anc	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(y\in \mathrm{dom}F⟼F\left(y\right)RC\right)$$
9	1	ffvelrnda	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)\in B$$
10	1	feqmptd	$$⊢\phi \to F=\left(y\in A⟼F\left(y\right)\right)$$
11		eqidd	$$⊢\phi \to \left(x\in B⟼xRC\right)=\left(x\in B⟼xRC\right)$$
12		oveq1	$$⊢x=F\left(y\right)\to xRC=F\left(y\right)RC$$
13	9 10 11 12	fmptco	$$⊢\phi \to \left(x\in B⟼xRC\right)\circ F=\left(y\in A⟼F\left(y\right)RC\right)$$
14	5 8 13	3eqtr4d	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(x\in B⟼xRC\right)\circ F$$