Theorem fmptco 5724

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

Hypotheses

Ref	Expression
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

Ref	Expression
fmptco	|- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Distinct variable groups:   x, A   x, y, B   y, R   ph, x   x, S   y, T

Allowed substitution hints:   ph( y)   A( y)   R( x)   S( y)   T( x)   F( x, y)   G( x, y)

Proof of Theorem fmptco

Dummy variables v u w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 5164	. 2 |- Rel ( G o. F )
2		funmpt 5292	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5271	. . 3 |- ( Fun ( x e. A |-> T ) -> Rel ( x e. A |-> T ) )
4	2, 3	ax-mp 5	. 2 |- Rel ( x e. A |-> T )
5		fmptco.1	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> R e. B )
6		eqid 2193	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 5712	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5390	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 167	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5406	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 14	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5595	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
14	13	imp 124	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
15	12, 14	sylan 283	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2199	. . . . . . . 8 |- ( ( ph /\ z F u ) -> u = ( F ` z ) )
17	16	a1d 22	. . . . . . 7 |- ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
18	17	expimpd 363	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 394	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1836	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		exsimpl 1628	. . . . . . 7 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> E. u u = ( F ` z ) )
22		isset 2766	. . . . . . 7 |- ( ( F ` z ) e. _V <-> E. u u = ( F ` z ) )
23	21, 22	sylibr 134	. . . . . 6 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> ( F ` z ) e. _V )
24	23	a1i 9	. . . . 5 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> ( F ` z ) e. _V ) )
25	12	adantr 276	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> Fun F )
26		fdm 5409	. . . . . . . . . . 11 |- ( F : A --> B -> dom F = A )
27	10, 26	syl 14	. . . . . . . . . 10 |- ( ph -> dom F = A )
28	27	eleq2d 2263	. . . . . . . . 9 |- ( ph -> ( z e. dom F <-> z e. A ) )
29	28	biimpar 297	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> z e. dom F )
30		funfvex 5571	. . . . . . . 8 |- ( ( Fun F /\ z e. dom F ) -> ( F ` z ) e. _V )
31	25, 29, 30	syl2anc 411	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( F ` z ) e. _V )
32	31	adantrr 479	. . . . . 6 |- ( ( ph /\ ( z e. A /\ w = [_ z / x ]_ T ) ) -> ( F ` z ) e. _V )
33	32	ex 115	. . . . 5 |- ( ph -> ( ( z e. A /\ w = [_ z / x ]_ T ) -> ( F ` z ) e. _V ) )
34		breq2 4033	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
35		breq1 4032	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
36	34, 35	anbi12d 473	. . . . . . . 8 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
37	36	ceqsexgv 2889	. . . . . . 7 |- ( ( F ` z ) e. _V -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
38		funfvbrb 5671	. . . . . . . . . . 11 |- ( Fun F -> ( z e. dom F <-> z F ( F ` z ) ) )
39	12, 38	syl 14	. . . . . . . . . 10 |- ( ph -> ( z e. dom F <-> z F ( F ` z ) ) )
40	39, 28	bitr3d 190	. . . . . . . . 9 |- ( ph -> ( z F ( F ` z ) <-> z e. A ) )
41	8	fveq1d 5556	. . . . . . . . . 10 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
42		fmptco.3	. . . . . . . . . 10 |- ( ph -> G = ( y e. B |-> S ) )
43		eqidd 2194	. . . . . . . . . 10 |- ( ph -> w = w )
44	41, 42, 43	breq123d 4043	. . . . . . . . 9 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
45	40, 44	anbi12d 473	. . . . . . . 8 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) ) )
46		nfcv 2336	. . . . . . . . . . 11 |- F/_ x z
47		nfv 1539	. . . . . . . . . . . 12 |- F/ x ph
48		nffvmpt1 5565	. . . . . . . . . . . . . 14 |- F/_ x ( ( x e. A |-> R ) ` z )
49		nfcv 2336	. . . . . . . . . . . . . 14 |- F/_ x ( y e. B |-> S )
50		nfcv 2336	. . . . . . . . . . . . . 14 |- F/_ x w
51	48, 49, 50	nfbr 4075	. . . . . . . . . . . . 13 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
52		nfcsb1v 3113	. . . . . . . . . . . . . 14 |- F/_ x [_ z / x ]_ T
53	52	nfeq2 2348	. . . . . . . . . . . . 13 |- F/ x w = [_ z / x ]_ T
54	51, 53	nfbi 1600	. . . . . . . . . . . 12 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
55	47, 54	nfim 1583	. . . . . . . . . . 11 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
56		fveq2 5554	. . . . . . . . . . . . . 14 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
57	56	breq1d 4039	. . . . . . . . . . . . 13 |- ( x = z -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
58		csbeq1a 3089	. . . . . . . . . . . . . 14 |- ( x = z -> T = [_ z / x ]_ T )
59	58	eqeq2d 2205	. . . . . . . . . . . . 13 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
60	57, 59	bibi12d 235	. . . . . . . . . . . 12 |- ( 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 ) ) )
61	60	imbi2d 230	. . . . . . . . . . 11 |- ( 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 ) ) ) )
62		vex 2763	. . . . . . . . . . . . . 14 |- w e. _V
63		simpl 109	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> y = R )
64	63	eleq1d 2262	. . . . . . . . . . . . . . . 16 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
65		simpr 110	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> u = w )
66		fmptco.4	. . . . . . . . . . . . . . . . . 18 |- ( y = R -> S = T )
67	66	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> S = T )
68	65, 67	eqeq12d 2208	. . . . . . . . . . . . . . . 16 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
69	64, 68	anbi12d 473	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
70		df-mpt 4092	. . . . . . . . . . . . . . 15 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
71	69, 70	brabga 4294	. . . . . . . . . . . . . 14 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
72	5, 62, 71	sylancl 413	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
73		simpr 110	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A ) -> x e. A )
74	6	fvmpt2 5641	. . . . . . . . . . . . . . 15 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
75	73, 5, 74	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
76	75	breq1d 4039	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
77	5	biantrurd 305	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
78	72, 76, 77	3bitr4d 220	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
79	78	expcom 116	. . . . . . . . . . 11 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
80	46, 55, 61, 79	vtoclgaf 2825	. . . . . . . . . 10 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
81	80	impcom 125	. . . . . . . . 9 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
82	81	pm5.32da 452	. . . . . . . 8 |- ( ph -> ( ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
83	45, 82	bitrd 188	. . . . . . 7 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
84	37, 83	sylan9bbr 463	. . . . . 6 |- ( ( ph /\ ( F ` z ) e. _V ) -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
85	84	ex 115	. . . . 5 |- ( ph -> ( ( F ` z ) e. _V -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) ) )
86	24, 33, 85	pm5.21ndd 706	. . . 4 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
87	20, 86	bitrd 188	. . 3 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
88		vex 2763	. . . 4 |- z e. _V
89	88, 62	opelco 4834	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
90		df-mpt 4092	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
91	90	eleq2i 2260	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
92		nfv 1539	. . . . . 6 |- F/ x z e. A
93	52	nfeq2 2348	. . . . . 6 |- F/ x v = [_ z / x ]_ T
94	92, 93	nfan 1576	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
95		nfv 1539	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
96		eleq1 2256	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
97	58	eqeq2d 2205	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
98	96, 97	anbi12d 473	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
99		eqeq1 2200	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
100	99	anbi2d 464	. . . . 5 |- ( v = w -> ( ( z e. A /\ v = [_ z / x ]_ T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
101	94, 95, 88, 62, 98, 100	opelopabf 4305	. . . 4 |- ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
102	91, 101	bitri 184	. . 3 |- ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
103	87, 89, 102	3bitr4g 223	. 2 |- ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
104	1, 4, 103	eqrelrdv 4755	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   E.wex 1503   e. wcel 2164   _Vcvv 2760   [_csb 3080   <.cop 3621   class class class wbr 4029   {copab 4089   |-> cmpt 4090   dom cdm 4659   o. ccom 4663   Rel wrel 4664   Fun wfun 5248   -->wf 5250   ` cfv 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-fv 5262

This theorem is referenced by:  fmptcof  5725  cofmpt  5727  fcompt  5728  fcoconst  5729  ofco  6149  gsumfzmhm2  13414  lmcn2  14448  cdivcncfap  14758  negfcncf  14760  dvcj  14858  dvfre  14859  dvmptcjx  14871