Theorem fmptco 6056

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 5333	. 2 |- Rel ( G o. F )
2		funmpt 5618	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5599	. . 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 2451	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 6046	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5714	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 236	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5731	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 17	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5903	. . . . . . . . . . 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 2457	. . . . . . . 8 |- ( ( ph /\ z F u ) -> u = ( F ` z ) )
17	16	a1d 26	. . . . . . 7 |- ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
18	17	expimpd 608	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 641	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1768	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		fvex 5875	. . . . . 6 |- ( F ` z ) e. _V
22		breq2 4406	. . . . . . 7 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
23		breq1 4405	. . . . . . 7 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
24	22, 23	anbi12d 717	. . . . . 6 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
25	21, 24	ceqsexv 3084	. . . . 5 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) )
26		funfvbrb 5995	. . . . . . . . 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 5733	. . . . . . . . . 10 |- ( F : A --> B -> dom F = A )
29	10, 28	syl 17	. . . . . . . . 9 |- ( ph -> dom F = A )
30	29	eleq2d 2514	. . . . . . . 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 5867	. . . . . . . 8 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
33		fmptco.3	. . . . . . . 8 |- ( ph -> G = ( y e. B |-> S ) )
34		eqidd 2452	. . . . . . . 8 |- ( ph -> w = w )
35	32, 33, 34	breq123d 4416	. . . . . . 7 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
36	31, 35	anbi12d 717	. . . . . 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 2592	. . . . . . . . 9 |- F/_ x z
38		nfv 1761	. . . . . . . . . 10 |- F/ x ph
39		nffvmpt1 5873	. . . . . . . . . . . 12 |- F/_ x ( ( x e. A |-> R ) ` z )
40		nfcv 2592	. . . . . . . . . . . 12 |- F/_ x ( y e. B |-> S )
41		nfcv 2592	. . . . . . . . . . . 12 |- F/_ x w
42	39, 40, 41	nfbr 4447	. . . . . . . . . . 11 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
43		nfcsb1v 3379	. . . . . . . . . . . 12 |- F/_ x [_ z / x ]_ T
44	43	nfeq2 2607	. . . . . . . . . . 11 |- F/ x w = [_ z / x ]_ T
45	42, 44	nfbi 2017	. . . . . . . . . 10 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
46	38, 45	nfim 2003	. . . . . . . . 9 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
47		fveq2 5865	. . . . . . . . . . . 12 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
48	47	breq1d 4412	. . . . . . . . . . 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 3372	. . . . . . . . . . . 12 |- ( x = z -> T = [_ z / x ]_ T )
50	49	eqeq2d 2461	. . . . . . . . . . 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 3048	. . . . . . . . . . . 12 |- w e. _V
54		simpl 459	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> y = R )
55	54	eleq1d 2513	. . . . . . . . . . . . . 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 2466	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
60	55, 59	anbi12d 717	. . . . . . . . . . . . 13 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
61		df-mpt 4463	. . . . . . . . . . . . 13 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
62	60, 61	brabga 4715	. . . . . . . . . . . 12 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
63	5, 53, 62	sylancl 668	. . . . . . . . . . 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 5957	. . . . . . . . . . . . 13 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
66	64, 5, 65	syl2anc 667	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
67	66	breq1d 4412	. . . . . . . . . . 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 3112	. . . . . . . 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 647	. . . . . 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 3048	. . . 4 |- z e. _V
78	77, 53	opelco 5006	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
79		df-mpt 4463	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
80	79	eleq2i 2521	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
81		nfv 1761	. . . . . 6 |- F/ x z e. A
82	43	nfeq2 2607	. . . . . 6 |- F/ x v = [_ z / x ]_ T
83	81, 82	nfan 2011	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
84		nfv 1761	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
85		eleq1 2517	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
86	49	eqeq2d 2461	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
87	85, 86	anbi12d 717	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
88		eqeq1 2455	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
89	88	anbi2d 710	. . . . 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 4726	. . . 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 4931	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1444   E.wex 1663   e. wcel 1887   _Vcvv 3045   [_csb 3363   <.cop 3974   class class class wbr 4402   {copab 4460   |-> cmpt 4461   dom cdm 4834   o. ccom 4838   Rel wrel 4839   Fun wfun 5576   -->wf 5578   ` cfv 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fv 5590

This theorem is referenced by:  fmptcof  6057  fcompt  6059  fcoconst  6060  ofco  6551  ccatco  12932  lo1o12  13597  rlimcn1  13652  rlimcn1b  13653  rlimdiv  13709  ackbijnn  13886  setcepi  15983  prf1st  16089  prf2nd  16090  hofcllem  16143  prdsidlem  16568  pws0g  16572  pwsco1mhm  16617  pwsco2mhm  16618  pwsinvg  16798  pwssub  16799  galactghm  17044  efginvrel1  17378  frgpup3lem  17427  gsumzf1o  17546  gsumconst  17567  gsummptshft  17569  gsumzmhm  17570  gsummhm2  17572  gsummptmhm  17573  gsumsub  17581  gsum2dlem2  17603  dprdfsub  17654  lmhmvsca  18268  psrass1lem  18601  psrlinv  18621  psrcom  18633  evlslem2  18735  coe1fval3  18801  psropprmul  18831  coe1z  18856  coe1mul2  18862  coe1tm  18866  ply1coe  18889  ply1coeOLD  18890  evls1sca  18912  frgpcyg  19144  evpmodpmf1o  19164  mhmvlin  19422  ofco2  19476  mdetleib2  19613  mdetralt  19633  smadiadetlem3  19693  ptrescn  20654  lmcn2  20664  qtopeu  20731  flfcnp2  21022  tgpconcomp  21127  tsmsmhm  21160  tsmssub  21163  tsmsxplem1  21167  negfcncf  21951  pcopt  22053  pcopt2  22054  pi1xfrcnvlem  22087  ovolctb  22443  ovolfs2  22523  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3  22543  ismbf  22586  mbfconst  22591  ismbfcn2  22595  itg1climres  22672  iblabslem  22785  iblabs  22786  bddmulibl  22796  limccnp  22846  limccnp2  22847  limcco  22848  dvcof  22902  dvcjbr  22903  dvcj  22904  dvfre  22905  dvmptcj  22922  dvmptco  22926  dvcnvlem  22928  dvef  22932  dvlip  22945  dvlipcn  22946  itgsubstlem  23000  plypf1  23166  plyco  23195  dgrcolem1  23227  dgrcolem2  23228  dgrco  23229  plycjlem  23230  taylply2  23323  logcn  23592  leibpi  23868  efrlim  23895  jensenlem2  23913  amgmlem  23915  lgamgulmlem2  23955  lgamcvg2  23980  ftalem7  24005  lgseisenlem4  24280  dchrisum0  24358  cofmpt  28266  ofcfval4  28926  eulerpartgbij  29205  dstfrvclim1  29310  cvmliftlem6  30013  cvmliftphtlem  30040  cvmlift3lem5  30046  elmsubrn  30166  msubco  30169  circum  30318  mblfinlem2  31978  volsupnfl  31985  itgaddnc  32002  itgmulc2nc  32010  ftc1anclem1  32017  ftc1anclem2  32018  ftc1anclem3  32019  ftc1anclem4  32020  ftc1anclem5  32021  ftc1anclem6  32022  ftc1anclem7  32023  ftc1anclem8  32024  fnopabco  32049  upixp  32056  mendassa  36060  cncfcompt  37760  dvcosax  37798  dirkercncflem4  37968  fourierdlem111  38081  meadjiunlem  38303  meadjiun  38304