# 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 syl5bb
` |-  ( 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 ) )`