This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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