Metamath Proof Explorer

Theorem fmpoco

Description: Composition of two functions. Variation of fmptco when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses fmpoco.1 
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> R e. C )
fmpoco.2 
|- ( ph -> F = ( x e. A , y e. B |-> R ) )
fmpoco.3 
|- ( ph -> G = ( z e. C |-> S ) )
fmpoco.4 
|- ( z = R -> S = T )
Assertion fmpoco 
|- ( ph -> ( G o. F ) = ( x e. A , y e. B |-> T ) )

Proof

Step Hyp Ref Expression
1 fmpoco.1 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> R e. C )
2 fmpoco.2 
 |-  ( ph -> F = ( x e. A , y e. B |-> R ) )
3 fmpoco.3 
 |-  ( ph -> G = ( z e. C |-> S ) )
4 fmpoco.4 
 |-  ( z = R -> S = T )
5 1 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. B R e. C )
6 eqid 
 |-  ( x e. A , y e. B |-> R ) = ( x e. A , y e. B |-> R )
7 6 fmpo 
 |-  ( A. x e. A A. y e. B R e. C <-> ( x e. A , y e. B |-> R ) : ( A X. B ) --> C )
8 5 7 sylib 
 |-  ( ph -> ( x e. A , y e. B |-> R ) : ( A X. B ) --> C )
9 nfcv 
 |-  F/_ u R
10 nfcv 
 |-  F/_ v R
11 nfcv 
 |-  F/_ x v
12 nfcsb1v 
 |-  F/_ x [_ u / x ]_ R
13 11 12 nfcsbw 
 |-  F/_ x [_ v / y ]_ [_ u / x ]_ R
14 nfcsb1v 
 |-  F/_ y [_ v / y ]_ [_ u / x ]_ R
15 csbeq1a 
 |-  ( x = u -> R = [_ u / x ]_ R )
16 csbeq1a 
 |-  ( y = v -> [_ u / x ]_ R = [_ v / y ]_ [_ u / x ]_ R )
17 15 16 sylan9eq 
 |-  ( ( x = u /\ y = v ) -> R = [_ v / y ]_ [_ u / x ]_ R )
18 9 10 13 14 17 cbvmpo 
 |-  ( x e. A , y e. B |-> R ) = ( u e. A , v e. B |-> [_ v / y ]_ [_ u / x ]_ R )
19 vex 
 |-  u e. _V
20 vex 
 |-  v e. _V
21 19 20 op2ndd 
 |-  ( w = <. u , v >. -> ( 2nd ` w ) = v )
22 21 csbeq1d 
 |-  ( w = <. u , v >. -> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R = [_ v / y ]_ [_ ( 1st ` w ) / x ]_ R )
23 19 20 op1std 
 |-  ( w = <. u , v >. -> ( 1st ` w ) = u )
24 23 csbeq1d 
 |-  ( w = <. u , v >. -> [_ ( 1st ` w ) / x ]_ R = [_ u / x ]_ R )
25 24 csbeq2dv 
 |-  ( w = <. u , v >. -> [_ v / y ]_ [_ ( 1st ` w ) / x ]_ R = [_ v / y ]_ [_ u / x ]_ R )
26 22 25 eqtrd 
 |-  ( w = <. u , v >. -> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R = [_ v / y ]_ [_ u / x ]_ R )
27 26 mpompt 
 |-  ( w e. ( A X. B ) |-> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R ) = ( u e. A , v e. B |-> [_ v / y ]_ [_ u / x ]_ R )
28 18 27 eqtr4i 
 |-  ( x e. A , y e. B |-> R ) = ( w e. ( A X. B ) |-> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R )
29 28 fmpt 
 |-  ( A. w e. ( A X. B ) [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R e. C <-> ( x e. A , y e. B |-> R ) : ( A X. B ) --> C )
30 8 29 sylibr 
 |-  ( ph -> A. w e. ( A X. B ) [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R e. C )
31 2 28 eqtrdi 
 |-  ( ph -> F = ( w e. ( A X. B ) |-> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R ) )
32 30 31 3 fmptcos 
 |-  ( ph -> ( G o. F ) = ( w e. ( A X. B ) |-> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S ) )
33 26 csbeq1d 
 |-  ( w = <. u , v >. -> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S = [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S )
34 33 mpompt 
 |-  ( w e. ( A X. B ) |-> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S ) = ( u e. A , v e. B |-> [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S )
35 nfcv 
 |-  F/_ u [_ R / z ]_ S
36 nfcv 
 |-  F/_ v [_ R / z ]_ S
37 nfcv 
 |-  F/_ x S
38 13 37 nfcsbw 
 |-  F/_ x [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S
39 nfcv 
 |-  F/_ y S
40 14 39 nfcsbw 
 |-  F/_ y [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S
41 17 csbeq1d 
 |-  ( ( x = u /\ y = v ) -> [_ R / z ]_ S = [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S )
42 35 36 38 40 41 cbvmpo 
 |-  ( x e. A , y e. B |-> [_ R / z ]_ S ) = ( u e. A , v e. B |-> [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S )
43 34 42 eqtr4i 
 |-  ( w e. ( A X. B ) |-> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S ) = ( x e. A , y e. B |-> [_ R / z ]_ S )
44 1 3impb 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> R e. C )
45 nfcvd 
 |-  ( R e. C -> F/_ z T )
46 45 4 csbiegf 
 |-  ( R e. C -> [_ R / z ]_ S = T )
47 44 46 syl 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> [_ R / z ]_ S = T )
48 47 mpoeq3dva 
 |-  ( ph -> ( x e. A , y e. B |-> [_ R / z ]_ S ) = ( x e. A , y e. B |-> T ) )
49 43 48 syl5eq 
 |-  ( ph -> ( w e. ( A X. B ) |-> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S ) = ( x e. A , y e. B |-> T ) )
50 32 49 eqtrd 
 |-  ( ph -> ( G o. F ) = ( x e. A , y e. B |-> T ) )