Theorem fmptcos

Description: Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	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)$$
Assertion	fmptcos	$$⊢\phi \to G\circ F=\left(x\in A⟼⦋R/y⦌S\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		nfcv	$$⊢\underset{\_}{Ⅎ}zS$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋z/y⦌S$$
6		csbeq1a	$$⊢y=z\to S=⦋z/y⦌S$$
7	4 5 6	cbvmpt	$$⊢\left(y\in B⟼S\right)=\left(z\in B⟼⦋z/y⦌S\right)$$
8	3 7	eqtrdi	$$⊢\phi \to G=\left(z\in B⟼⦋z/y⦌S\right)$$
9		csbeq1	$$⊢z=R\to ⦋z/y⦌S=⦋R/y⦌S$$
10	1 2 8 9	fmptcof	$$⊢\phi \to G\circ F=\left(x\in A⟼⦋R/y⦌S\right)$$