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