Metamath Proof Explorer


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 ) )