Theorem fmpoco

Description: Composition of two functions. Variation of fmptco when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	fmpoco.1	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to R\in C$$
	fmpoco.2	$$⊢\phi \to F=\left(x\in A,y\in B⟼R\right)$$
	fmpoco.3	$$⊢\phi \to G=\left(z\in C⟼S\right)$$
	fmpoco.4	$$⊢z=R\to S=T$$
Assertion	fmpoco	$$⊢\phi \to G\circ F=\left(x\in A,y\in B⟼T\right)$$

Proof

Step	Hyp	Ref	Expression
1		fmpoco.1	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to R\in C$$
2		fmpoco.2	$$⊢\phi \to F=\left(x\in A,y\in B⟼R\right)$$
3		fmpoco.3	$$⊢\phi \to G=\left(z\in C⟼S\right)$$
4		fmpoco.4	$$⊢z=R\to S=T$$
5	1	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in BR\in C$$
6		eqid	$$⊢\left(x\in A,y\in B⟼R\right)=\left(x\in A,y\in B⟼R\right)$$
7	6	fmpo	$$⊢\forall x\in A\forall y\in BR\in C\leftrightarrow \left(x\in A,y\in B⟼R\right):A\times B⟶C$$
8	5 7	sylib	$$⊢\phi \to \left(x\in A,y\in B⟼R\right):A\times B⟶C$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}uR$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}vR$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}xv$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋u/x⦌R$$
13	11 12	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋v/y⦌⦋u/x⦌R$$
14		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋v/y⦌⦋u/x⦌R$$
15		csbeq1a	$$⊢x=u\to R=⦋u/x⦌R$$
16		csbeq1a	$$⊢y=v\to ⦋u/x⦌R=⦋v/y⦌⦋u/x⦌R$$
17	15 16	sylan9eq	$$⊢\left(x=u\wedge y=v\right)\to R=⦋v/y⦌⦋u/x⦌R$$
18	9 10 13 14 17	cbvmpo	$$⊢\left(x\in A,y\in B⟼R\right)=\left(u\in A,v\in B⟼⦋v/y⦌⦋u/x⦌R\right)$$
19		vex	$$⊢u\in \mathrm{V}$$
20		vex	$$⊢v\in \mathrm{V}$$
21	19 20	op2ndd	$$⊢w=⟨u,v⟩\to 2^{nd}\left(w\right)=v$$
22	21	csbeq1d	$$⊢w=⟨u,v⟩\to ⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R=⦋v/y⦌⦋1^{st}\left(w\right)/x⦌R$$
23	19 20	op1std	$$⊢w=⟨u,v⟩\to 1^{st}\left(w\right)=u$$
24	23	csbeq1d	$$⊢w=⟨u,v⟩\to ⦋1^{st}\left(w\right)/x⦌R=⦋u/x⦌R$$
25	24	csbeq2dv	$$⊢w=⟨u,v⟩\to ⦋v/y⦌⦋1^{st}\left(w\right)/x⦌R=⦋v/y⦌⦋u/x⦌R$$
26	22 25	eqtrd	$$⊢w=⟨u,v⟩\to ⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R=⦋v/y⦌⦋u/x⦌R$$
27	26	mpompt	$$⊢\left(w\in \left(A\times B\right)⟼⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R\right)=\left(u\in A,v\in B⟼⦋v/y⦌⦋u/x⦌R\right)$$
28	18 27	eqtr4i	$$⊢\left(x\in A,y\in B⟼R\right)=\left(w\in \left(A\times B\right)⟼⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R\right)$$
29	28	fmpt	$$⊢\forall w\in \left(A\times B\right)⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R\in C\leftrightarrow \left(x\in A,y\in B⟼R\right):A\times B⟶C$$
30	8 29	sylibr	$$⊢\phi \to \forall w\in \left(A\times B\right)⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R\in C$$
31	2 28	eqtrdi	$$⊢\phi \to F=\left(w\in \left(A\times B\right)⟼⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R\right)$$
32	30 31 3	fmptcos	$$⊢\phi \to G\circ F=\left(w\in \left(A\times B\right)⟼⦋⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R/z⦌S\right)$$
33	26	csbeq1d	$$⊢w=⟨u,v⟩\to ⦋⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R/z⦌S=⦋⦋v/y⦌⦋u/x⦌R/z⦌S$$
34	33	mpompt	$$⊢\left(w\in \left(A\times B\right)⟼⦋⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R/z⦌S\right)=\left(u\in A,v\in B⟼⦋⦋v/y⦌⦋u/x⦌R/z⦌S\right)$$
35		nfcv	$$⊢\underset{\_}{Ⅎ}u⦋R/z⦌S$$
36		nfcv	$$⊢\underset{\_}{Ⅎ}v⦋R/z⦌S$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}xS$$
38	13 37	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋⦋v/y⦌⦋u/x⦌R/z⦌S$$
39		nfcv	$$⊢\underset{\_}{Ⅎ}yS$$
40	14 39	nfcsbw	$$⊢\underset{\_}{Ⅎ}y⦋⦋v/y⦌⦋u/x⦌R/z⦌S$$
41	17	csbeq1d	$$⊢\left(x=u\wedge y=v\right)\to ⦋R/z⦌S=⦋⦋v/y⦌⦋u/x⦌R/z⦌S$$
42	35 36 38 40 41	cbvmpo	$$⊢\left(x\in A,y\in B⟼⦋R/z⦌S\right)=\left(u\in A,v\in B⟼⦋⦋v/y⦌⦋u/x⦌R/z⦌S\right)$$
43	34 42	eqtr4i	$$⊢\left(w\in \left(A\times B\right)⟼⦋⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R/z⦌S\right)=\left(x\in A,y\in B⟼⦋R/z⦌S\right)$$
44	1	3impb	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to R\in C$$
45		nfcvd	$$⊢R\in C\to \underset{\_}{Ⅎ}zT$$
46	45 4	csbiegf	$$⊢R\in C\to ⦋R/z⦌S=T$$
47	44 46	syl	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to ⦋R/z⦌S=T$$
48	47	mpoeq3dva	$$⊢\phi \to \left(x\in A,y\in B⟼⦋R/z⦌S\right)=\left(x\in A,y\in B⟼T\right)$$
49	43 48	eqtrid	$$⊢\phi \to \left(w\in \left(A\times B\right)⟼⦋⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R/z⦌S\right)=\left(x\in A,y\in B⟼T\right)$$
50	32 49	eqtrd	$$⊢\phi \to G\circ F=\left(x\in A,y\in B⟼T\right)$$