Metamath Proof Explorer

Theorem fmptcof

Description: Version of fmptco where ph needn't be distinct from x . (Contributed by NM, 27-Dec-2014)

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 ) )
fmptcof.4 
|- ( y = R -> S = T )
Assertion fmptcof 
|- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

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 fmptcof.4 
 |-  ( y = R -> S = T )
5 nfcsb1v 
 |-  F/_ x [_ z / x ]_ R
6 5 nfel1 
 |-  F/ x [_ z / x ]_ R e. B
7 csbeq1a 
 |-  ( x = z -> R = [_ z / x ]_ R )
8 7 eleq1d 
 |-  ( x = z -> ( R e. B <-> [_ z / x ]_ R e. B ) )
9 6 8 rspc 
 |-  ( z e. A -> ( A. x e. A R e. B -> [_ z / x ]_ R e. B ) )
10 1 9 mpan9 
 |-  ( ( ph /\ z e. A ) -> [_ z / x ]_ R e. B )
11 nfcv 
 |-  F/_ z R
12 11 5 7 cbvmpt 
 |-  ( x e. A |-> R ) = ( z e. A |-> [_ z / x ]_ R )
13 2 12 eqtrdi 
 |-  ( ph -> F = ( z e. A |-> [_ z / x ]_ R ) )
14 nfcv 
 |-  F/_ w S
15 nfcsb1v 
 |-  F/_ y [_ w / y ]_ S
16 csbeq1a 
 |-  ( y = w -> S = [_ w / y ]_ S )
17 14 15 16 cbvmpt 
 |-  ( y e. B |-> S ) = ( w e. B |-> [_ w / y ]_ S )
18 3 17 eqtrdi 
 |-  ( ph -> G = ( w e. B |-> [_ w / y ]_ S ) )
19 csbeq1 
 |-  ( w = [_ z / x ]_ R -> [_ w / y ]_ S = [_ [_ z / x ]_ R / y ]_ S )
20 10 13 18 19 fmptco 
 |-  ( ph -> ( G o. F ) = ( z e. A |-> [_ [_ z / x ]_ R / y ]_ S ) )
21 nfcv 
 |-  F/_ z [_ R / y ]_ S
22 nfcv 
 |-  F/_ x S
23 5 22 nfcsbw 
 |-  F/_ x [_ [_ z / x ]_ R / y ]_ S
24 7 csbeq1d 
 |-  ( x = z -> [_ R / y ]_ S = [_ [_ z / x ]_ R / y ]_ S )
25 21 23 24 cbvmpt 
 |-  ( x e. A |-> [_ R / y ]_ S ) = ( z e. A |-> [_ [_ z / x ]_ R / y ]_ S )
26 20 25 eqtr4di 
 |-  ( ph -> ( G o. F ) = ( x e. A |-> [_ R / y ]_ S ) )
27 eqid 
 |-  A = A
28 nfcvd 
 |-  ( R e. B -> F/_ y T )
29 28 4 csbiegf 
 |-  ( R e. B -> [_ R / y ]_ S = T )
30 29 ralimi 
 |-  ( A. x e. A R e. B -> A. x e. A [_ R / y ]_ S = T )
31 mpteq12 
 |-  ( ( A = A /\ A. x e. A [_ R / y ]_ S = T ) -> ( x e. A |-> [_ R / y ]_ S ) = ( x e. A |-> T ) )
32 27 30 31 sylancr 
 |-  ( A. x e. A R e. B -> ( x e. A |-> [_ R / y ]_ S ) = ( x e. A |-> T ) )
33 1 32 syl 
 |-  ( ph -> ( x e. A |-> [_ R / y ]_ S ) = ( x e. A |-> T ) )
34 26 33 eqtrd 
 |-  ( ph -> ( G o. F ) = ( x e. A |-> T ) )