Theorem ofoprabco

Description: Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Hypotheses	ofoprabco.1	$$⊢\underset{\_}{Ⅎ}aM$$
	ofoprabco.2	$$⊢\phi \to F:A⟶B$$
	ofoprabco.3	$$⊢\phi \to G:A⟶C$$
	ofoprabco.4	$$⊢\phi \to A\in V$$
	ofoprabco.5	$$⊢\phi \to M=\left(a\in A⟼⟨F\left(a\right),G\left(a\right)⟩\right)$$
	ofoprabco.6	$$⊢\phi \to N=\left(x\in B,y\in C⟼xRy\right)$$
Assertion	ofoprabco	$$⊢\phi \to F{R}_{f}G=N\circ M$$

Proof

Step	Hyp	Ref	Expression
1		ofoprabco.1	$$⊢\underset{\_}{Ⅎ}aM$$
2		ofoprabco.2	$$⊢\phi \to F:A⟶B$$
3		ofoprabco.3	$$⊢\phi \to G:A⟶C$$
4		ofoprabco.4	$$⊢\phi \to A\in V$$
5		ofoprabco.5	$$⊢\phi \to M=\left(a\in A⟼⟨F\left(a\right),G\left(a\right)⟩\right)$$
6		ofoprabco.6	$$⊢\phi \to N=\left(x\in B,y\in C⟼xRy\right)$$
7	2	ffvelrnda	$$⊢\left(\phi \wedge a\in A\right)\to F\left(a\right)\in B$$
8	3	ffvelrnda	$$⊢\left(\phi \wedge a\in A\right)\to G\left(a\right)\in C$$
9		opelxpi	$$⊢\left(F\left(a\right)\in B\wedge G\left(a\right)\in C\right)\to ⟨F\left(a\right),G\left(a\right)⟩\in \left(B\times C\right)$$
10	7 8 9	syl2anc	$$⊢\left(\phi \wedge a\in A\right)\to ⟨F\left(a\right),G\left(a\right)⟩\in \left(B\times C\right)$$
11	5 10	fvmpt2d	$$⊢\left(\phi \wedge a\in A\right)\to M\left(a\right)=⟨F\left(a\right),G\left(a\right)⟩$$
12	11	fveq2d	$$⊢\left(\phi \wedge a\in A\right)\to N\left(M\left(a\right)\right)=N\left(⟨F\left(a\right),G\left(a\right)⟩\right)$$
13		df-ov	$$⊢F\left(a\right)NG\left(a\right)=N\left(⟨F\left(a\right),G\left(a\right)⟩\right)$$
14	13	a1i	$$⊢\left(\phi \wedge a\in A\right)\to F\left(a\right)NG\left(a\right)=N\left(⟨F\left(a\right),G\left(a\right)⟩\right)$$
15	6	adantr	$$⊢\left(\phi \wedge a\in A\right)\to N=\left(x\in B,y\in C⟼xRy\right)$$
16		simprl	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge \left(x=F\left(a\right)\wedge y=G\left(a\right)\right)\right)\to x=F\left(a\right)$$
17		simprr	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge \left(x=F\left(a\right)\wedge y=G\left(a\right)\right)\right)\to y=G\left(a\right)$$
18	16 17	oveq12d	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge \left(x=F\left(a\right)\wedge y=G\left(a\right)\right)\right)\to xRy=F\left(a\right)RG\left(a\right)$$
19		ovexd	$$⊢\left(\phi \wedge a\in A\right)\to F\left(a\right)RG\left(a\right)\in \mathrm{V}$$
20	15 18 7 8 19	ovmpod	$$⊢\left(\phi \wedge a\in A\right)\to F\left(a\right)NG\left(a\right)=F\left(a\right)RG\left(a\right)$$
21	12 14 20	3eqtr2d	$$⊢\left(\phi \wedge a\in A\right)\to N\left(M\left(a\right)\right)=F\left(a\right)RG\left(a\right)$$
22	21	mpteq2dva	$$⊢\phi \to \left(a\in A⟼N\left(M\left(a\right)\right)\right)=\left(a\in A⟼F\left(a\right)RG\left(a\right)\right)$$
23		ovex	$$⊢xRy\in \mathrm{V}$$
24	23	rgen2w	$$⊢\forall x\in B\forall y\in CxRy\in \mathrm{V}$$
25		eqid	$$⊢\left(x\in B,y\in C⟼xRy\right)=\left(x\in B,y\in C⟼xRy\right)$$
26	25	fmpo	$$⊢\forall x\in B\forall y\in CxRy\in \mathrm{V}\leftrightarrow \left(x\in B,y\in C⟼xRy\right):B\times C⟶\mathrm{V}$$
27	24 26	mpbi	$$⊢\left(x\in B,y\in C⟼xRy\right):B\times C⟶\mathrm{V}$$
28	6	feq1d	$$⊢\phi \to \left(N:B\times C⟶\mathrm{V}\leftrightarrow \left(x\in B,y\in C⟼xRy\right):B\times C⟶\mathrm{V}\right)$$
29	27 28	mpbiri	$$⊢\phi \to N:B\times C⟶\mathrm{V}$$
30	5 10	fmpt3d	$$⊢\phi \to M:A⟶B\times C$$
31	1	fcomptf	$$⊢\left(N:B\times C⟶\mathrm{V}\wedge M:A⟶B\times C\right)\to N\circ M=\left(a\in A⟼N\left(M\left(a\right)\right)\right)$$
32	29 30 31	syl2anc	$$⊢\phi \to N\circ M=\left(a\in A⟼N\left(M\left(a\right)\right)\right)$$
33	2	feqmptd	$$⊢\phi \to F=\left(a\in A⟼F\left(a\right)\right)$$
34	3	feqmptd	$$⊢\phi \to G=\left(a\in A⟼G\left(a\right)\right)$$
35	4 7 8 33 34	offval2	$$⊢\phi \to F{R}_{f}G=\left(a\in A⟼F\left(a\right)RG\left(a\right)\right)$$
36	22 32 35	3eqtr4rd	$$⊢\phi \to F{R}_{f}G=N\circ M$$