Metamath Proof Explorer

Theorem fmpocos

Description: Composition of two functions. Variation of fmpoco with more context in the substitution hypothesis for T . (Contributed by SN, 14-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 fmpocos.1 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> R e. C )
2 fmpocos.2 
 |-  ( ph -> F = ( x e. A , y e. B |-> R ) )
3 fmpocos.3 
 |-  ( ph -> G = ( z e. C |-> S ) )
4 fmpocos.4 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> [_ R / z ]_ 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 19 20 op1std 
 |-  ( w = <. u , v >. -> ( 1st ` w ) = u )
23 22 csbeq1d 
 |-  ( w = <. u , v >. -> [_ ( 1st ` w ) / x ]_ R = [_ u / x ]_ R )
24 21 23 csbeq12dv 
 |-  ( w = <. u , v >. -> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R = [_ v / y ]_ [_ u / x ]_ R )
25 24 mpompt 
 |-  ( w e. ( A X. B ) |-> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R ) = ( u e. A , v e. B |-> [_ v / y ]_ [_ u / x ]_ R )
26 18 25 eqtr4i 
 |-  ( x e. A , y e. B |-> R ) = ( w e. ( A X. B ) |-> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R )
27 26 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 )
28 8 27 sylibr 
 |-  ( ph -> A. w e. ( A X. B ) [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R e. C )
29 2 26 eqtrdi 
 |-  ( ph -> F = ( w e. ( A X. B ) |-> [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R ) )
30 28 29 3 fmptcos 
 |-  ( ph -> ( G o. F ) = ( w e. ( A X. B ) |-> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S ) )
31 24 csbeq1d 
 |-  ( w = <. u , v >. -> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S = [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S )
32 31 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 )
33 nfcv 
 |-  F/_ u [_ R / z ]_ S
34 nfcv 
 |-  F/_ v [_ R / z ]_ S
35 nfcv 
 |-  F/_ x S
36 13 35 nfcsbw 
 |-  F/_ x [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S
37 nfcv 
 |-  F/_ y S
38 14 37 nfcsbw 
 |-  F/_ y [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S
39 17 csbeq1d 
 |-  ( ( x = u /\ y = v ) -> [_ R / z ]_ S = [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S )
40 33 34 36 38 39 cbvmpo 
 |-  ( x e. A , y e. B |-> [_ R / z ]_ S ) = ( u e. A , v e. B |-> [_ [_ v / y ]_ [_ u / x ]_ R / z ]_ S )
41 32 40 eqtr4i 
 |-  ( w e. ( A X. B ) |-> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S ) = ( x e. A , y e. B |-> [_ R / z ]_ S )
42 4 3impb 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> [_ R / z ]_ S = T )
43 42 mpoeq3dva 
 |-  ( ph -> ( x e. A , y e. B |-> [_ R / z ]_ S ) = ( x e. A , y e. B |-> T ) )
44 41 43 eqtrid 
 |-  ( ph -> ( w e. ( A X. B ) |-> [_ [_ ( 2nd ` w ) / y ]_ [_ ( 1st ` w ) / x ]_ R / z ]_ S ) = ( x e. A , y e. B |-> T ) )
45 30 44 eqtrd 
 |-  ( ph -> ( G o. F ) = ( x e. A , y e. B |-> T ) )