Theorem fmptco 6049

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 5495	. 2 |- Rel ( G o. F )
2		funmpt 5614	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5595	. . 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 2443	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 6040	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5707	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 232	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5723	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 16	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5896	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
14	13	imp 429	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
15	12, 14	sylan 471	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2451	. . . . . . . 8 |- ( ( ph /\ z F u ) -> u = ( F ` z ) )
17	16	a1d 25	. . . . . . 7 |- ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
18	17	expimpd 603	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 635	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1701	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		fvex 5866	. . . . . 6 |- ( F ` z ) e. _V
22		breq2 4441	. . . . . . 7 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
23		breq1 4440	. . . . . . 7 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
24	22, 23	anbi12d 710	. . . . . 6 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
25	21, 24	ceqsexv 3132	. . . . 5 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) )
26		funfvbrb 5985	. . . . . . . . 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 5725	. . . . . . . . . 10 |- ( F : A --> B -> dom F = A )
29	10, 28	syl 16	. . . . . . . . 9 |- ( ph -> dom F = A )
30	29	eleq2d 2513	. . . . . . . 8 |- ( ph -> ( z e. dom F <-> z e. A ) )
31	27, 30	bitr3d 255	. . . . . . 7 |- ( ph -> ( z F ( F ` z ) <-> z e. A ) )
32	8	fveq1d 5858	. . . . . . . 8 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
33		fmptco.3	. . . . . . . 8 |- ( ph -> G = ( y e. B |-> S ) )
34		eqidd 2444	. . . . . . . 8 |- ( ph -> w = w )
35	32, 33, 34	breq123d 4451	. . . . . . 7 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
36	31, 35	anbi12d 710	. . . . . 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 2605	. . . . . . . . 9 |- F/_ x z
38		nfv 1694	. . . . . . . . . 10 |- F/ x ph
39		nffvmpt1 5864	. . . . . . . . . . . 12 |- F/_ x ( ( x e. A |-> R ) ` z )
40		nfcv 2605	. . . . . . . . . . . 12 |- F/_ x ( y e. B |-> S )
41		nfcv 2605	. . . . . . . . . . . 12 |- F/_ x w
42	39, 40, 41	nfbr 4481	. . . . . . . . . . 11 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
43		nfcsb1v 3436	. . . . . . . . . . . 12 |- F/_ x [_ z / x ]_ T
44	43	nfeq2 2622	. . . . . . . . . . 11 |- F/ x w = [_ z / x ]_ T
45	42, 44	nfbi 1920	. . . . . . . . . 10 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
46	38, 45	nfim 1906	. . . . . . . . 9 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
47		fveq2 5856	. . . . . . . . . . . 12 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
48	47	breq1d 4447	. . . . . . . . . . 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 3429	. . . . . . . . . . . 12 |- ( x = z -> T = [_ z / x ]_ T )
50	49	eqeq2d 2457	. . . . . . . . . . 11 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
51	48, 50	bibi12d 321	. . . . . . . . . 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 316	. . . . . . . . 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 3098	. . . . . . . . . . . 12 |- w e. _V
54		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> y = R )
55	54	eleq1d 2512	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
56		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> u = w )
57		fmptco.4	. . . . . . . . . . . . . . . 16 |- ( y = R -> S = T )
58	57	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> S = T )
59	56, 58	eqeq12d 2465	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
60	55, 59	anbi12d 710	. . . . . . . . . . . . 13 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
61		df-mpt 4497	. . . . . . . . . . . . 13 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
62	60, 61	brabga 4751	. . . . . . . . . . . 12 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
63	5, 53, 62	sylancl 662	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
64		simpr 461	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> x e. A )
65	6	fvmpt2 5948	. . . . . . . . . . . . 13 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
66	64, 5, 65	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
67	66	breq1d 4447	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
68	5	biantrurd 508	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
69	63, 67, 68	3bitr4d 285	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
70	69	expcom 435	. . . . . . . . 9 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
71	37, 46, 52, 70	vtoclgaf 3158	. . . . . . . 8 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
72	71	impcom 430	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
73	72	pm5.32da 641	. . . . . 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 253	. . . . 5 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
75	25, 74	syl5bb 257	. . . 4 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
76	20, 75	bitrd 253	. . 3 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
77		vex 3098	. . . 4 |- z e. _V
78	77, 53	opelco 5164	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
79		df-mpt 4497	. . . . 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 1694	. . . . . 6 |- F/ x z e. A
82	43	nfeq2 2622	. . . . . 6 |- F/ x v = [_ z / x ]_ T
83	81, 82	nfan 1914	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
84		nfv 1694	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
85		eleq1 2515	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
86	49	eqeq2d 2457	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
87	85, 86	anbi12d 710	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
88		eqeq1 2447	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
89	88	anbi2d 703	. . . . 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 4762	. . . 4 |- ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
91	80, 90	bitri 249	. . 3 |- ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
92	76, 78, 91	3bitr4g 288	. 2 |- ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
93	1, 4, 92	eqrelrdv 5089	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1383   E.wex 1599   e. wcel 1804   _Vcvv 3095   [_csb 3420   <.cop 4020   class class class wbr 4437   {copab 4494   |-> cmpt 4495   dom cdm 4989   o. ccom 4993   Rel wrel 4994   Fun wfun 5572   -->wf 5574   ` cfv 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586

This theorem is referenced by:  fmptcof  6050  fcompt  6052  fcoconst  6053  ofco  6545  ccatco  12783  lo1o12  13338  rlimcn1  13393  rlimcn1b  13394  rlimdiv  13450  ackbijnn  13622  setcepi  15394  prf1st  15452  prf2nd  15453  hofcllem  15506  prdsidlem  15931  pws0g  15935  pwsco1mhm  15980  pwsco2mhm  15981  pwsinvg  16161  pwssub  16162  galactghm  16407  efginvrel1  16725  frgpup3lem  16774  gsumzf1o  16896  gsumzf1oOLD  16899  gsumconst  16933  gsummptshft  16935  gsumzmhm  16936  gsumzmhmOLD  16937  gsummhm2  16940  gsummhm2OLD  16941  gsummptmhm  16942  gsumsub  16953  gsumsubOLD  16954  gsum2dlem2  16977  gsum2dOLD  16979  dprdfsub  17040  dprdfsubOLD  17047  lmhmvsca  17670  psrass1lem  18008  psrlinv  18029  psrcom  18043  evlslem2  18159  coe1fval3  18226  psropprmul  18258  coe1z  18283  coe1mul2  18289  coe1tm  18293  ply1coe  18316  ply1coeOLD  18317  evls1sca  18339  frgpcyg  18590  evpmodpmf1o  18610  mhmvlin  18877  ofco2  18931  mdetleib2  19068  mdetralt  19088  smadiadetlem3  19148  ptrescn  20118  lmcn2  20128  qtopeu  20195  flfcnp2  20486  tgpconcomp  20589  tsmsmhm  20626  tsmssub  20629  tsmsxplem1  20633  negfcncf  21401  pcopt  21500  pcopt2  21501  pi1xfrcnvlem  21534  ovolctb  21879  ovolfs2  21958  uniioombllem2  21970  uniioombllem3  21972  ismbf  22015  mbfconst  22020  ismbfcn2  22024  itg1climres  22099  iblabslem  22212  iblabs  22213  bddmulibl  22223  limccnp  22273  limccnp2  22274  limcco  22275  dvcof  22329  dvcjbr  22330  dvcj  22331  dvfre  22332  dvmptcj  22349  dvmptco  22353  dvcnvlem  22355  dvef  22359  dvlip  22372  dvlipcn  22373  itgsubstlem  22427  plypf1  22587  plyco  22616  dgrcolem1  22648  dgrcolem2  22649  dgrco  22650  plycjlem  22651  taylply2  22741  logcn  23006  leibpi  23251  efrlim  23277  jensenlem2  23295  amgmlem  23297  ftalem7  23330  lgseisenlem4  23605  dchrisum0  23683  cofmpt  27482  ofcfval4  28082  eulerpartgbij  28289  dstfrvclim1  28394  lgamgulmlem2  28550  lgamcvg2  28575  cvmliftlem6  28713  cvmliftphtlem  28740  cvmlift3lem5  28746  elmsubrn  28866  msubco  28869  circum  29018  mblfinlem2  30028  volsupnfl  30035  itgaddnc  30051  itgmulc2nc  30059  ftc1anclem1  30066  ftc1anclem2  30067  ftc1anclem3  30068  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  fnopabco  30189  upixp  30196  mendassa  31119  cncfcompt  31639  dvcosax  31677  dirkercncflem4  31842  fourierdlem111  31954