Theorem fmptco 5860

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 5327	. 2 |- Rel ( G o. F )
2		funmpt 5448	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5430	. . 3 |- ( Fun ( x e. A |-> T ) -> Rel ( x e. A |-> T ) )
4	2, 3	ax-mp 8	. 2 |- Rel ( x e. A |-> T )
5		fmptco.1	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> R e. B )
6		eqid 2404	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 5852	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5539	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 224	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5552	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 16	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5724	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
14	13	imp 419	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
15	12, 14	sylan 458	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2409	. . . . . . . 8 |- ( ( ph /\ z F u ) -> u = ( F ` z ) )
17	16	a1d 23	. . . . . . 7 |- ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
18	17	expimpd 587	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 617	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1633	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		fvex 5701	. . . . . 6 |- ( F ` z ) e. _V
22		breq2 4176	. . . . . . 7 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
23		breq1 4175	. . . . . . 7 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
24	22, 23	anbi12d 692	. . . . . 6 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
25	21, 24	ceqsexv 2951	. . . . 5 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) )
26		funfvbrb 5802	. . . . . . . . 9 |- ( Fun F -> ( z e. dom F <-> z F ( F ` z ) ) )
27	12, 26	syl 16	. . . . . . . 8 |- ( ph -> ( z e. dom F <-> z F ( F ` z ) ) )
28		fdm 5554	. . . . . . . . . 10 |- ( F : A --> B -> dom F = A )
29	10, 28	syl 16	. . . . . . . . 9 |- ( ph -> dom F = A )
30	29	eleq2d 2471	. . . . . . . 8 |- ( ph -> ( z e. dom F <-> z e. A ) )
31	27, 30	bitr3d 247	. . . . . . 7 |- ( ph -> ( z F ( F ` z ) <-> z e. A ) )
32	8	fveq1d 5689	. . . . . . . 8 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
33		fmptco.3	. . . . . . . 8 |- ( ph -> G = ( y e. B |-> S ) )
34		eqidd 2405	. . . . . . . 8 |- ( ph -> w = w )
35	32, 33, 34	breq123d 4186	. . . . . . 7 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
36	31, 35	anbi12d 692	. . . . . 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 2540	. . . . . . . . 9 |- F/_ x z
38		nfv 1626	. . . . . . . . . 10 |- F/ x ph
39		nffvmpt1 5695	. . . . . . . . . . . 12 |- F/_ x ( ( x e. A |-> R ) ` z )
40		nfcv 2540	. . . . . . . . . . . 12 |- F/_ x ( y e. B |-> S )
41		nfcv 2540	. . . . . . . . . . . 12 |- F/_ x w
42	39, 40, 41	nfbr 4216	. . . . . . . . . . 11 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
43		nfcsb1v 3243	. . . . . . . . . . . 12 |- F/_ x [_ z / x ]_ T
44	43	nfeq2 2551	. . . . . . . . . . 11 |- F/ x w = [_ z / x ]_ T
45	42, 44	nfbi 1852	. . . . . . . . . 10 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
46	38, 45	nfim 1828	. . . . . . . . 9 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
47		fveq2 5687	. . . . . . . . . . . 12 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
48	47	breq1d 4182	. . . . . . . . . . 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 3219	. . . . . . . . . . . 12 |- ( x = z -> T = [_ z / x ]_ T )
50	49	eqeq2d 2415	. . . . . . . . . . 11 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
51	48, 50	bibi12d 313	. . . . . . . . . 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 308	. . . . . . . . 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 2919	. . . . . . . . . . . 12 |- w e. _V
54		simpl 444	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> y = R )
55	54	eleq1d 2470	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
56		simpr 448	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> u = w )
57		fmptco.4	. . . . . . . . . . . . . . . 16 |- ( y = R -> S = T )
58	57	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> S = T )
59	56, 58	eqeq12d 2418	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
60	55, 59	anbi12d 692	. . . . . . . . . . . . 13 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
61		df-mpt 4228	. . . . . . . . . . . . 13 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
62	60, 61	brabga 4429	. . . . . . . . . . . 12 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
63	5, 53, 62	sylancl 644	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
64		simpr 448	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> x e. A )
65	6	fvmpt2 5771	. . . . . . . . . . . . 13 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
66	64, 5, 65	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
67	66	breq1d 4182	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
68	5	biantrurd 495	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
69	63, 67, 68	3bitr4d 277	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
70	69	expcom 425	. . . . . . . . 9 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
71	37, 46, 52, 70	vtoclgaf 2976	. . . . . . . 8 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
72	71	impcom 420	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
73	72	pm5.32da 623	. . . . . 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 245	. . . . 5 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
75	25, 74	syl5bb 249	. . . 4 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
76	20, 75	bitrd 245	. . 3 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
77		vex 2919	. . . 4 |- z e. _V
78	77, 53	opelco 5003	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
79		df-mpt 4228	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
80	79	eleq2i 2468	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
81		nfv 1626	. . . . . 6 |- F/ x z e. A
82	43	nfeq2 2551	. . . . . 6 |- F/ x v = [_ z / x ]_ T
83	81, 82	nfan 1842	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
84		nfv 1626	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
85		eleq1 2464	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
86	49	eqeq2d 2415	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
87	85, 86	anbi12d 692	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
88		eqeq1 2410	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
89	88	anbi2d 685	. . . . 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 4439	. . . 4 |- ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
91	80, 90	bitri 241	. . 3 |- ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
92	76, 78, 91	3bitr4g 280	. 2 |- ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
93	1, 4, 92	eqrelrdv 4931	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   E.wex 1547   = wceq 1649   e. wcel 1721   _Vcvv 2916   [_csb 3211   <.cop 3777   class class class wbr 4172   {copab 4225   e. cmpt 4226   dom cdm 4837   o. ccom 4841   Rel wrel 4842   Fun wfun 5407   -->wf 5409   ` cfv 5413

This theorem is referenced by:  fmptcof  5861  fcompt  5863  fcoconst  5864  ofco  6283  ccatco  11759  lo1o12  12282  rlimcn1  12337  rlimcn1b  12338  rlimdiv  12394  ackbijnn  12562  setcepi  14198  prf1st  14256  prf2nd  14257  hofcllem  14310  prdsidlem  14682  pws0g  14686  pwsco1mhm  14724  pwsco2mhm  14725  pwsinvg  14885  pwssub  14886  galactghm  15061  efginvrel1  15315  frgpup3lem  15364  gsumzf1o  15474  gsumconst  15487  gsumzmhm  15488  gsummhm2  15490  gsumsub  15497  gsum2d  15501  dprdfsub  15534  lmhmvsca  16076  psrass1lem  16397  psrlinv  16416  psrcom  16427  evlslem2  16523  coe1fval3  16561  psropprmul  16587  coe1z  16611  coe1mul2  16617  coe1tm  16620  ply1coe  16639  frgpcyg  16809  ptrescn  17624  lmcn2  17634  qtopeu  17701  flfcnp2  17992  tgpconcomp  18095  tsmsmhm  18128  tsmssub  18131  tsmsxplem1  18135  negfcncf  18902  pcopt  19000  pcopt2  19001  pi1xfrcnvlem  19034  ovolctb  19339  ovolfs2  19416  uniioombllem2  19428  uniioombllem3  19430  ismbf  19475  mbfconst  19480  ismbfcn2  19484  itg1climres  19559  iblabslem  19672  iblabs  19673  bddmulibl  19683  limccnp  19731  limccnp2  19732  limcco  19733  dvcof  19787  dvcjbr  19788  dvcj  19789  dvfre  19790  dvmptcj  19807  dvmptco  19811  dvcnvlem  19813  dvef  19817  dvlip  19830  dvlipcn  19831  itgsubstlem  19885  plypf1  20084  plyco  20113  dgrcolem1  20144  dgrcolem2  20145  dgrco  20146  plycjlem  20147  taylply2  20237  logcn  20491  leibpi  20735  efrlim  20761  jensenlem2  20779  amgmlem  20781  ftalem7  20814  lgseisenlem4  21089  dchrisum0  21167  cofmpt  24031  ofcfval4  24441  dstfrvclim1  24688  lgamgulmlem2  24767  lgamcvg2  24792  cvmliftlem6  24930  cvmliftphtlem  24957  cvmlift3lem5  24963  circum  25064  mblfinlem  26143  volsupnfl  26150  itgaddnc  26164  itgmulc2nc  26172  fnopabco  26314  upixp  26321  mhmvlin  27320  mendassa  27370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421