Metamath Proof Explorer

Theorem fmptco

Description: Composition of two functions expressed as ordered-pair class abstractions. If F has the equation ( x + 2 ) and G the equation ( 3 * z ) then ( G o. F ) has the equation ( 3 * ( x + 2 ) ) . (Contributed by FL, 21-Jun-2012) (Revised by Mario Carneiro, 24-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 fmptco.1 
 |-  ( ( ph /\ x e. A ) -> R e. B )
2 fmptco.2 
 |-  ( ph -> F = ( x e. A |-> R ) )
3 fmptco.3 
 |-  ( ph -> G = ( y e. B |-> S ) )
4 fmptco.4 
 |-  ( y = R -> S = T )
5 relco 
 |-  Rel ( G o. F )
6 mptrel 
 |-  Rel ( x e. A |-> T )
7 2 1 fmpt3d 
 |-  ( ph -> F : A --> B )
8 7 ffund 
 |-  ( ph -> Fun F )
9 funbrfv 
 |-  ( Fun F -> ( z F u -> ( F ` z ) = u ) )
10 9 imp 
 |-  ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
11 8 10 sylan 
 |-  ( ( ph /\ z F u ) -> ( F ` z ) = u )
12 11 eqcomd 
 |-  ( ( ph /\ z F u ) -> u = ( F ` z ) )
13 12 a1d 
 |-  ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
14 13 expimpd 
 |-  ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
15 14 pm4.71rd 
 |-  ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
16 15 exbidv 
 |-  ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
17 fvex 
 |-  ( F ` z ) e. _V
18 breq2 
 |-  ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
19 breq1 
 |-  ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
20 18 19 anbi12d 
 |-  ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
21 17 20 ceqsexv 
 |-  ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) )
22 funfvbrb 
 |-  ( Fun F -> ( z e. dom F <-> z F ( F ` z ) ) )
23 8 22 syl 
 |-  ( ph -> ( z e. dom F <-> z F ( F ` z ) ) )
24 7 fdmd 
 |-  ( ph -> dom F = A )
25 24 eleq2d 
 |-  ( ph -> ( z e. dom F <-> z e. A ) )
26 23 25 bitr3d 
 |-  ( ph -> ( z F ( F ` z ) <-> z e. A ) )
27 2 fveq1d 
 |-  ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
28 eqidd 
 |-  ( ph -> w = w )
29 27 3 28 breq123d 
 |-  ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
30 26 29 anbi12d 
 |-  ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) ) )
31 nfcv 
 |-  F/_ x z
32 nfv 
 |-  F/ x ph
33 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> R ) ` z )
34 nfcv 
 |-  F/_ x ( y e. B |-> S )
35 nfcv 
 |-  F/_ x w
36 33 34 35 nfbr 
 |-  F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
37 nfcsb1v 
 |-  F/_ x [_ z / x ]_ T
38 37 nfeq2 
 |-  F/ x w = [_ z / x ]_ T
39 36 38 nfbi 
 |-  F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
40 32 39 nfim 
 |-  F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
41 fveq2 
 |-  ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
42 41 breq1d 
 |-  ( x = z -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
43 csbeq1a 
 |-  ( x = z -> T = [_ z / x ]_ T )
44 43 eqeq2d 
 |-  ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
45 42 44 bibi12d 
 |-  ( x = z -> ( ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) <-> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
46 45 imbi2d 
 |-  ( x = z -> ( ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) <-> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) ) )
47 vex 
 |-  w e. _V
48 simpl 
 |-  ( ( y = R /\ u = w ) -> y = R )
49 48 eleq1d 
 |-  ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
50 id 
 |-  ( u = w -> u = w )
51 50 4 eqeqan12rd 
 |-  ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
52 49 51 anbi12d 
 |-  ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
53 df-mpt 
 |-  ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
54 52 53 brabga 
 |-  ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
55 1 47 54 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
56 id 
 |-  ( x e. A -> x e. A )
57 eqid 
 |-  ( x e. A |-> R ) = ( x e. A |-> R )
58 57 fvmpt2 
 |-  ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
59 56 1 58 syl2an2 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
60 59 breq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
61 1 biantrurd 
 |-  ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
62 55 60 61 3bitr4d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
63 62 expcom 
 |-  ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
64 31 40 46 63 vtoclgaf 
 |-  ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
65 64 impcom 
 |-  ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
66 65 pm5.32da 
 |-  ( ph -> ( ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
67 30 66 bitrd 
 |-  ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
68 21 67 bitrid 
 |-  ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
69 16 68 bitrd 
 |-  ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
70 vex 
 |-  z e. _V
71 70 47 opelco 
 |-  ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
72 df-mpt 
 |-  ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
73 72 eleq2i 
 |-  ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
74 nfv 
 |-  F/ x z e. A
75 37 nfeq2 
 |-  F/ x v = [_ z / x ]_ T
76 74 75 nfan 
 |-  F/ x ( z e. A /\ v = [_ z / x ]_ T )
77 nfv 
 |-  F/ v ( z e. A /\ w = [_ z / x ]_ T )
78 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
79 43 eqeq2d 
 |-  ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
80 78 79 anbi12d 
 |-  ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
81 eqeq1 
 |-  ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
82 81 anbi2d 
 |-  ( v = w -> ( ( z e. A /\ v = [_ z / x ]_ T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
83 76 77 70 47 80 82 opelopabf 
 |-  ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
84 73 83 bitri 
 |-  ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
85 69 71 84 3bitr4g 
 |-  ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
86 5 6 85 eqrelrdv 
 |-  ( ph -> ( G o. F ) = ( x e. A |-> T ) )