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	|- ( ph -> A. x e. A R e. B )
	fmptcof.2	|- ( ph -> F = ( x e. A |-> R ) )
	fmptcof.3	|- ( ph -> G = ( y e. B |-> S ) )
Assertion	fmptcos	|- ( ph -> ( G o. F ) = ( x e. A |-> [_ R / y ]_ S ) )

Proof

Step	Hyp	Ref	Expression
1		fmptcof.1	|- ( ph -> A. x e. A R e. B )
2		fmptcof.2	|- ( ph -> F = ( x e. A |-> R ) )
3		fmptcof.3	|- ( ph -> G = ( y e. B |-> S ) )
4		nfcv	|- F/_ z S
5		nfcsb1v	|- F/_ y [_ z / y ]_ S
6		csbeq1a	|- ( y = z -> S = [_ z / y ]_ S )
7	4 5 6	cbvmpt	|- ( y e. B |-> S ) = ( z e. B |-> [_ z / y ]_ S )
8	3 7	eqtrdi	|- ( ph -> G = ( z e. B |-> [_ z / y ]_ S ) )
9		csbeq1	|- ( z = R -> [_ z / y ]_ S = [_ R / y ]_ S )
10	1 2 8 9	fmptcof	|- ( ph -> ( G o. F ) = ( x e. A |-> [_ R / y ]_ S ) )