Theorem fmptco 5801

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 5227	. 2 |- Rel ( G o. F )
2		funmpt 5356	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5335	. . 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 2229	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 5789	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5460	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 167	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5476	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 14	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5670	. . . . . . . . . . 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 2235	. . . . . . . 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 1871	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		exsimpl 1663	. . . . . . 7 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> E. u u = ( F ` z ) )
22		isset 2806	. . . . . . 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 5479	. . . . . . . . . . 11 |- ( F : A --> B -> dom F = A )
27	10, 26	syl 14	. . . . . . . . . 10 |- ( ph -> dom F = A )
28	27	eleq2d 2299	. . . . . . . . 9 |- ( ph -> ( z e. dom F <-> z e. A ) )
29	28	biimpar 297	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> z e. dom F )
30		funfvex 5644	. . . . . . . 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 4087	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
35		breq1 4086	. . . . . . . . 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 2932	. . . . . . 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 5748	. . . . . . . . . . 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 5629	. . . . . . . . . 10 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
42		fmptco.3	. . . . . . . . . 10 |- ( ph -> G = ( y e. B |-> S ) )
43		eqidd 2230	. . . . . . . . . 10 |- ( ph -> w = w )
44	41, 42, 43	breq123d 4097	. . . . . . . . 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 2372	. . . . . . . . . . 11 |- F/_ x z
47		nfv 1574	. . . . . . . . . . . 12 |- F/ x ph
48		nffvmpt1 5638	. . . . . . . . . . . . . 14 |- F/_ x ( ( x e. A |-> R ) ` z )
49		nfcv 2372	. . . . . . . . . . . . . 14 |- F/_ x ( y e. B |-> S )
50		nfcv 2372	. . . . . . . . . . . . . 14 |- F/_ x w
51	48, 49, 50	nfbr 4130	. . . . . . . . . . . . 13 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
52		nfcsb1v 3157	. . . . . . . . . . . . . 14 |- F/_ x [_ z / x ]_ T
53	52	nfeq2 2384	. . . . . . . . . . . . 13 |- F/ x w = [_ z / x ]_ T
54	51, 53	nfbi 1635	. . . . . . . . . . . 12 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
55	47, 54	nfim 1618	. . . . . . . . . . 11 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
56		fveq2 5627	. . . . . . . . . . . . . 14 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
57	56	breq1d 4093	. . . . . . . . . . . . 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 3133	. . . . . . . . . . . . . 14 |- ( x = z -> T = [_ z / x ]_ T )
59	58	eqeq2d 2241	. . . . . . . . . . . . 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 2802	. . . . . . . . . . . . . 14 |- w e. _V
63		simpl 109	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> y = R )
64	63	eleq1d 2298	. . . . . . . . . . . . . . . 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 2244	. . . . . . . . . . . . . . . 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 4147	. . . . . . . . . . . . . . 15 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
71	69, 70	brabga 4352	. . . . . . . . . . . . . 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 5718	. . . . . . . . . . . . . . 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 4093	. . . . . . . . . . . . 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 2866	. . . . . . . . . 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 710	. . . 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 2802	. . . 4 |- z e. _V
89	88, 62	opelco 4894	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
90		df-mpt 4147	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
91	90	eleq2i 2296	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
92		nfv 1574	. . . . . 6 |- F/ x z e. A
93	52	nfeq2 2384	. . . . . 6 |- F/ x v = [_ z / x ]_ T
94	92, 93	nfan 1611	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
95		nfv 1574	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
96		eleq1 2292	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
97	58	eqeq2d 2241	. . . . . 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 2236	. . . . . 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 4363	. . . 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 4815	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1395   E.wex 1538   e. wcel 2200   _Vcvv 2799   [_csb 3124   <.cop 3669   class class class wbr 4083   {copab 4144   |-> cmpt 4145   dom cdm 4719   o. ccom 4723   Rel wrel 4724   Fun wfun 5312   -->wf 5314   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326

This theorem is referenced by:  fmptcof  5802  cofmpt  5804  fcompt  5805  fcoconst  5806  ofco  6237  prdsidlem  13480  pws0g  13484  pwsinvg  13645  pwssub  13646  gsumfzmhm2  13881  psrlinv  14648  lmcn2  14954  cdivcncfap  15278  negfcncf  15280  dvcj  15383  dvfre  15384  dvmptcjx  15398  plyco  15433  plycjlemc  15434