Metamath Proof Explorer

Theorem fmptcof2

Description: Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012) (Revised by Mario Carneiro, 24-Jul-2014) (Revised by Thierry Arnoux, 10-May-2017)

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

Proof

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