Theorem fmpocos

Description: Composition of two functions. Variation of fmpoco with more context in the substitution hypothesis for T . (Contributed by SN, 14-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fmpocos.1	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to R\in C$$
2		fmpocos.2	$$⊢\phi \to F=\left(x\in A,y\in B⟼R\right)$$
3		fmpocos.3	$$⊢\phi \to G=\left(z\in C⟼S\right)$$
4		fmpocos.4	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to ⦋R/z⦌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	19 20	op1std	$$⊢w=⟨u,v⟩\to 1^{st}\left(w\right)=u$$
23	22	csbeq1d	$$⊢w=⟨u,v⟩\to ⦋1^{st}\left(w\right)/x⦌R=⦋u/x⦌R$$
24	21 23	csbeq12dv	$$⊢w=⟨u,v⟩\to ⦋2^{nd}\left(w\right)/y⦌⦋1^{st}\left(w\right)/x⦌R=⦋v/y⦌⦋u/x⦌R$$
25	24	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)$$
26	18 25	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)$$
27	26	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$$
28	8 27	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$$
29	2 26	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)$$
30	28 29 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)$$
31	24	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$$
32	31	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)$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}u⦋R/z⦌S$$
34		nfcv	$$⊢\underset{\_}{Ⅎ}v⦋R/z⦌S$$
35		nfcv	$$⊢\underset{\_}{Ⅎ}xS$$
36	13 35	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋⦋v/y⦌⦋u/x⦌R/z⦌S$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}yS$$
38	14 37	nfcsbw	$$⊢\underset{\_}{Ⅎ}y⦋⦋v/y⦌⦋u/x⦌R/z⦌S$$
39	17	csbeq1d	$$⊢\left(x=u\wedge y=v\right)\to ⦋R/z⦌S=⦋⦋v/y⦌⦋u/x⦌R/z⦌S$$
40	33 34 36 38 39	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)$$
41	32 40	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)$$
42	4	3impb	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to ⦋R/z⦌S=T$$
43	42	mpoeq3dva	$$⊢\phi \to \left(x\in A,y\in B⟼⦋R/z⦌S\right)=\left(x\in A,y\in B⟼T\right)$$
44	41 43	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)$$
45	30 44	eqtrd	$$⊢\phi \to G\circ F=\left(x\in A,y\in B⟼T\right)$$