Theorem fmptco 6069

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 5350	. 2 |- Rel ( G o. F )
2		funmpt 5635	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5616	. . 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 2423	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 6059	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5730	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 236	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5746	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 17	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5917	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
14	13	imp 431	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
15	12, 14	sylan 474	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2431	. . . . . . . 8 |- ( ( ph /\ z F u ) -> u = ( F ` z ) )
17	16	a1d 27	. . . . . . 7 |- ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
18	17	expimpd 607	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 640	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1759	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		fvex 5889	. . . . . 6 |- ( F ` z ) e. _V
22		breq2 4425	. . . . . . 7 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
23		breq1 4424	. . . . . . 7 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
24	22, 23	anbi12d 716	. . . . . 6 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
25	21, 24	ceqsexv 3119	. . . . 5 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) )
26		funfvbrb 6008	. . . . . . . . 9 |- ( Fun F -> ( z e. dom F <-> z F ( F ` z ) ) )
27	12, 26	syl 17	. . . . . . . 8 |- ( ph -> ( z e. dom F <-> z F ( F ` z ) ) )
28		fdm 5748	. . . . . . . . . 10 |- ( F : A --> B -> dom F = A )
29	10, 28	syl 17	. . . . . . . . 9 |- ( ph -> dom F = A )
30	29	eleq2d 2493	. . . . . . . 8 |- ( ph -> ( z e. dom F <-> z e. A ) )
31	27, 30	bitr3d 259	. . . . . . 7 |- ( ph -> ( z F ( F ` z ) <-> z e. A ) )
32	8	fveq1d 5881	. . . . . . . 8 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
33		fmptco.3	. . . . . . . 8 |- ( ph -> G = ( y e. B |-> S ) )
34		eqidd 2424	. . . . . . . 8 |- ( ph -> w = w )
35	32, 33, 34	breq123d 4435	. . . . . . 7 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
36	31, 35	anbi12d 716	. . . . . 6 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) ) )
37		nfcv 2585	. . . . . . . . 9 |- F/_ x z
38		nfv 1752	. . . . . . . . . 10 |- F/ x ph
39		nffvmpt1 5887	. . . . . . . . . . . 12 |- F/_ x ( ( x e. A |-> R ) ` z )
40		nfcv 2585	. . . . . . . . . . . 12 |- F/_ x ( y e. B |-> S )
41		nfcv 2585	. . . . . . . . . . . 12 |- F/_ x w
42	39, 40, 41	nfbr 4466	. . . . . . . . . . 11 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
43		nfcsb1v 3412	. . . . . . . . . . . 12 |- F/_ x [_ z / x ]_ T
44	43	nfeq2 2602	. . . . . . . . . . 11 |- F/ x w = [_ z / x ]_ T
45	42, 44	nfbi 1991	. . . . . . . . . 10 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
46	38, 45	nfim 1977	. . . . . . . . 9 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
47		fveq2 5879	. . . . . . . . . . . 12 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
48	47	breq1d 4431	. . . . . . . . . . 11 |- ( x = z -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
49		csbeq1a 3405	. . . . . . . . . . . 12 |- ( x = z -> T = [_ z / x ]_ T )
50	49	eqeq2d 2437	. . . . . . . . . . 11 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
51	48, 50	bibi12d 323	. . . . . . . . . 10 |- ( 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 ) ) )
52	51	imbi2d 318	. . . . . . . . 9 |- ( 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 ) ) ) )
53		vex 3085	. . . . . . . . . . . 12 |- w e. _V
54		simpl 459	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> y = R )
55	54	eleq1d 2492	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
56		simpr 463	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> u = w )
57		fmptco.4	. . . . . . . . . . . . . . . 16 |- ( y = R -> S = T )
58	57	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> S = T )
59	56, 58	eqeq12d 2445	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
60	55, 59	anbi12d 716	. . . . . . . . . . . . 13 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
61		df-mpt 4482	. . . . . . . . . . . . 13 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
62	60, 61	brabga 4732	. . . . . . . . . . . 12 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
63	5, 53, 62	sylancl 667	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
64		simpr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> x e. A )
65	6	fvmpt2 5971	. . . . . . . . . . . . 13 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
66	64, 5, 65	syl2anc 666	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
67	66	breq1d 4431	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
68	5	biantrurd 511	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
69	63, 67, 68	3bitr4d 289	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
70	69	expcom 437	. . . . . . . . 9 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
71	37, 46, 52, 70	vtoclgaf 3145	. . . . . . . 8 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
72	71	impcom 432	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
73	72	pm5.32da 646	. . . . . 6 |- ( ph -> ( ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
74	36, 73	bitrd 257	. . . . 5 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
75	25, 74	syl5bb 261	. . . 4 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
76	20, 75	bitrd 257	. . 3 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
77		vex 3085	. . . 4 |- z e. _V
78	77, 53	opelco 5023	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
79		df-mpt 4482	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
80	79	eleq2i 2501	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
81		nfv 1752	. . . . . 6 |- F/ x z e. A
82	43	nfeq2 2602	. . . . . 6 |- F/ x v = [_ z / x ]_ T
83	81, 82	nfan 1985	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
84		nfv 1752	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
85		eleq1 2495	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
86	49	eqeq2d 2437	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
87	85, 86	anbi12d 716	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
88		eqeq1 2427	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
89	88	anbi2d 709	. . . . 5 |- ( v = w -> ( ( z e. A /\ v = [_ z / x ]_ T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
90	83, 84, 77, 53, 87, 89	opelopabf 4743	. . . 4 |- ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
91	80, 90	bitri 253	. . 3 |- ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
92	76, 78, 91	3bitr4g 292	. 2 |- ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
93	1, 4, 92	eqrelrdv 4948	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1438   E.wex 1660   e. wcel 1869   _Vcvv 3082   [_csb 3396   <.cop 4003   class class class wbr 4421   {copab 4479   |-> cmpt 4480   dom cdm 4851   o. ccom 4855   Rel wrel 4856   Fun wfun 5593   -->wf 5595   ` cfv 5599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-fv 5607

This theorem is referenced by:  fmptcof  6070  fcompt  6072  fcoconst  6073  ofco  6563  ccatco  12928  lo1o12  13590  rlimcn1  13645  rlimcn1b  13646  rlimdiv  13702  ackbijnn  13879  setcepi  15976  prf1st  16082  prf2nd  16083  hofcllem  16136  prdsidlem  16561  pws0g  16565  pwsco1mhm  16610  pwsco2mhm  16611  pwsinvg  16791  pwssub  16792  galactghm  17037  efginvrel1  17371  frgpup3lem  17420  gsumzf1o  17539  gsumconst  17560  gsummptshft  17562  gsumzmhm  17563  gsummhm2  17565  gsummptmhm  17566  gsumsub  17574  gsum2dlem2  17596  dprdfsub  17647  lmhmvsca  18261  psrass1lem  18594  psrlinv  18614  psrcom  18626  evlslem2  18728  coe1fval3  18794  psropprmul  18824  coe1z  18849  coe1mul2  18855  coe1tm  18859  ply1coe  18882  ply1coeOLD  18883  evls1sca  18905  frgpcyg  19136  evpmodpmf1o  19156  mhmvlin  19414  ofco2  19468  mdetleib2  19605  mdetralt  19625  smadiadetlem3  19685  ptrescn  20646  lmcn2  20656  qtopeu  20723  flfcnp2  21014  tgpconcomp  21119  tsmsmhm  21152  tsmssub  21155  tsmsxplem1  21159  negfcncf  21943  pcopt  22045  pcopt2  22046  pi1xfrcnvlem  22079  ovolctb  22435  ovolfs2  22515  uniioombllem2  22532  uniioombllem2OLD  22533  uniioombllem3  22535  ismbf  22578  mbfconst  22583  ismbfcn2  22587  itg1climres  22664  iblabslem  22777  iblabs  22778  bddmulibl  22788  limccnp  22838  limccnp2  22839  limcco  22840  dvcof  22894  dvcjbr  22895  dvcj  22896  dvfre  22897  dvmptcj  22914  dvmptco  22918  dvcnvlem  22920  dvef  22924  dvlip  22937  dvlipcn  22938  itgsubstlem  22992  plypf1  23158  plyco  23187  dgrcolem1  23219  dgrcolem2  23220  dgrco  23221  plycjlem  23222  taylply2  23315  logcn  23584  leibpi  23860  efrlim  23887  jensenlem2  23905  amgmlem  23907  lgamgulmlem2  23947  lgamcvg2  23972  ftalem7  23997  lgseisenlem4  24272  dchrisum0  24350  cofmpt  28262  ofcfval4  28928  eulerpartgbij  29207  dstfrvclim1  29312  cvmliftlem6  30015  cvmliftphtlem  30042  cvmlift3lem5  30048  elmsubrn  30168  msubco  30171  circum  30320  mblfinlem2  31936  volsupnfl  31943  itgaddnc  31960  itgmulc2nc  31968  ftc1anclem1  31975  ftc1anclem2  31976  ftc1anclem3  31977  ftc1anclem4  31978  ftc1anclem5  31979  ftc1anclem6  31980  ftc1anclem7  31981  ftc1anclem8  31982  fnopabco  32007  upixp  32014  mendassa  36024  cncfcompt  37624  dvcosax  37662  dirkercncflem4  37832  fourierdlem111  37945  meadjiunlem  38126  meadjiun  38127