Theorem fmptcof

Description: Version of fmptco where ph needn't be distinct from x . (Contributed by NM, 27-Dec-2014)

	Ref	Expression
Hypotheses	fmptcof.1	$$⊢\phi \to \forall x\in AR\in B$$
	fmptcof.2	$$⊢\phi \to F=\left(x\in A⟼R\right)$$
	fmptcof.3	$$⊢\phi \to G=\left(y\in B⟼S\right)$$
	fmptcof.4	$$⊢y=R\to S=T$$
Assertion	fmptcof	$$⊢\phi \to G\circ F=\left(x\in A⟼T\right)$$

Proof

Step	Hyp	Ref	Expression
1		fmptcof.1	$$⊢\phi \to \forall x\in AR\in B$$
2		fmptcof.2	$$⊢\phi \to F=\left(x\in A⟼R\right)$$
3		fmptcof.3	$$⊢\phi \to G=\left(y\in B⟼S\right)$$
4		fmptcof.4	$$⊢y=R\to S=T$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌R$$
6	5	nfel1	$$⊢Ⅎx⦋z/x⦌R\in B$$
7		csbeq1a	$$⊢x=z\to R=⦋z/x⦌R$$
8	7	eleq1d	$$⊢x=z\to \left(R\in B\leftrightarrow ⦋z/x⦌R\in B\right)$$
9	6 8	rspc	$$⊢z\in A\to \left(\forall x\in AR\in B\to ⦋z/x⦌R\in B\right)$$
10	1 9	mpan9	$$⊢\left(\phi \wedge z\in A\right)\to ⦋z/x⦌R\in B$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}zR$$
12	11 5 7	cbvmpt	$$⊢\left(x\in A⟼R\right)=\left(z\in A⟼⦋z/x⦌R\right)$$
13	2 12	syl6eq	$$⊢\phi \to F=\left(z\in A⟼⦋z/x⦌R\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}wS$$
15		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋w/y⦌S$$
16		csbeq1a	$$⊢y=w\to S=⦋w/y⦌S$$
17	14 15 16	cbvmpt	$$⊢\left(y\in B⟼S\right)=\left(w\in B⟼⦋w/y⦌S\right)$$
18	3 17	syl6eq	$$⊢\phi \to G=\left(w\in B⟼⦋w/y⦌S\right)$$
19		csbeq1	$$⊢w=⦋z/x⦌R\to ⦋w/y⦌S=⦋⦋z/x⦌R/y⦌S$$
20	10 13 18 19	fmptco	$$⊢\phi \to G\circ F=\left(z\in A⟼⦋⦋z/x⦌R/y⦌S\right)$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}z⦋R/y⦌S$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}xS$$
23	5 22	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋⦋z/x⦌R/y⦌S$$
24	7	csbeq1d	$$⊢x=z\to ⦋R/y⦌S=⦋⦋z/x⦌R/y⦌S$$
25	21 23 24	cbvmpt	$$⊢\left(x\in A⟼⦋R/y⦌S\right)=\left(z\in A⟼⦋⦋z/x⦌R/y⦌S\right)$$
26	20 25	eqtr4di	$$⊢\phi \to G\circ F=\left(x\in A⟼⦋R/y⦌S\right)$$
27		eqid	$$⊢A=A$$
28		nfcvd	$$⊢R\in B\to \underset{\_}{Ⅎ}yT$$
29	28 4	csbiegf	$$⊢R\in B\to ⦋R/y⦌S=T$$
30	29	ralimi	$$⊢\forall x\in AR\in B\to \forall x\in A⦋R/y⦌S=T$$
31		mpteq12	$$⊢\left(A=A\wedge \forall x\in A⦋R/y⦌S=T\right)\to \left(x\in A⟼⦋R/y⦌S\right)=\left(x\in A⟼T\right)$$
32	27 30 31	sylancr	$$⊢\forall x\in AR\in B\to \left(x\in A⟼⦋R/y⦌S\right)=\left(x\in A⟼T\right)$$
33	1 32	syl	$$⊢\phi \to \left(x\in A⟼⦋R/y⦌S\right)=\left(x\in A⟼T\right)$$
34	26 33	eqtrd	$$⊢\phi \to G\circ F=\left(x\in A⟼T\right)$$