Theorem fmptco 5979

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 5426	. 2 |- Rel ( G o. F )
2		funmpt 5545	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5526	. . 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 2392	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 5970	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5638	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 232	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5654	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 16	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5825	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
14	13	imp 427	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
15	12, 14	sylan 469	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2400	. . . . . . . 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 601	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 633	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1729	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		fvex 5797	. . . . . 6 |- ( F ` z ) e. _V
22		breq2 4384	. . . . . . 7 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
23		breq1 4383	. . . . . . 7 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
24	22, 23	anbi12d 708	. . . . . 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 5915	. . . . . . . . 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 5656	. . . . . . . . . 10 |- ( F : A --> B -> dom F = A )
29	10, 28	syl 16	. . . . . . . . 9 |- ( ph -> dom F = A )
30	29	eleq2d 2462	. . . . . . . 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 5789	. . . . . . . 8 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
33		fmptco.3	. . . . . . . 8 |- ( ph -> G = ( y e. B |-> S ) )
34		eqidd 2393	. . . . . . . 8 |- ( ph -> w = w )
35	32, 33, 34	breq123d 4394	. . . . . . 7 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
36	31, 35	anbi12d 708	. . . . . 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 2554	. . . . . . . . 9 |- F/_ x z
38		nfv 1722	. . . . . . . . . 10 |- F/ x ph
39		nffvmpt1 5795	. . . . . . . . . . . 12 |- F/_ x ( ( x e. A |-> R ) ` z )
40		nfcv 2554	. . . . . . . . . . . 12 |- F/_ x ( y e. B |-> S )
41		nfcv 2554	. . . . . . . . . . . 12 |- F/_ x w
42	39, 40, 41	nfbr 4424	. . . . . . . . . . 11 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
43		nfcsb1v 3377	. . . . . . . . . . . 12 |- F/_ x [_ z / x ]_ T
44	43	nfeq2 2571	. . . . . . . . . . 11 |- F/ x w = [_ z / x ]_ T
45	42, 44	nfbi 1952	. . . . . . . . . 10 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
46	38, 45	nfim 1938	. . . . . . . . 9 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
47		fveq2 5787	. . . . . . . . . . . 12 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
48	47	breq1d 4390	. . . . . . . . . . 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 3370	. . . . . . . . . . . 12 |- ( x = z -> T = [_ z / x ]_ T )
50	49	eqeq2d 2406	. . . . . . . . . . 11 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
51	48, 50	bibi12d 319	. . . . . . . . . 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 314	. . . . . . . . 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 3050	. . . . . . . . . . . 12 |- w e. _V
54		simpl 455	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> y = R )
55	54	eleq1d 2461	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
56		simpr 459	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> u = w )
57		fmptco.4	. . . . . . . . . . . . . . . 16 |- ( y = R -> S = T )
58	57	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> S = T )
59	56, 58	eqeq12d 2414	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
60	55, 59	anbi12d 708	. . . . . . . . . . . . 13 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
61		df-mpt 4440	. . . . . . . . . . . . 13 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
62	60, 61	brabga 4688	. . . . . . . . . . . 12 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
63	5, 53, 62	sylancl 660	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
64		simpr 459	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> x e. A )
65	6	fvmpt2 5878	. . . . . . . . . . . . 13 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
66	64, 5, 65	syl2anc 659	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
67	66	breq1d 4390	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
68	5	biantrurd 506	. . . . . . . . . . 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 433	. . . . . . . . 9 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
71	37, 46, 52, 70	vtoclgaf 3110	. . . . . . . 8 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
72	71	impcom 428	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
73	72	pm5.32da 639	. . . . . 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 3050	. . . 4 |- z e. _V
78	77, 53	opelco 5100	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
79		df-mpt 4440	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
80	79	eleq2i 2470	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
81		nfv 1722	. . . . . 6 |- F/ x z e. A
82	43	nfeq2 2571	. . . . . 6 |- F/ x v = [_ z / x ]_ T
83	81, 82	nfan 1946	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
84		nfv 1722	. . . . 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 2406	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
87	85, 86	anbi12d 708	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
88		eqeq1 2396	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
89	88	anbi2d 701	. . . . 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 4699	. . . 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 5025	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   E.wex 1627   e. wcel 1836   _Vcvv 3047   [_csb 3361   <.cop 3963   class class class wbr 4380   {copab 4437   |-> cmpt 4438   dom cdm 4926   o. ccom 4930   Rel wrel 4931   Fun wfun 5503   -->wf 5505   ` cfv 5509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-fv 5517

This theorem is referenced by:  fmptcof  5980  fcompt  5982  fcoconst  5983  ofco  6477  ccatco  12731  lo1o12  13377  rlimcn1  13432  rlimcn1b  13433  rlimdiv  13489  ackbijnn  13661  setcepi  15503  prf1st  15609  prf2nd  15610  hofcllem  15663  prdsidlem  16088  pws0g  16092  pwsco1mhm  16137  pwsco2mhm  16138  pwsinvg  16318  pwssub  16319  galactghm  16564  efginvrel1  16882  frgpup3lem  16931  gsumzf1o  17053  gsumzf1oOLD  17056  gsumconst  17089  gsummptshft  17091  gsumzmhm  17092  gsumzmhmOLD  17093  gsummhm2  17096  gsummhm2OLD  17097  gsummptmhm  17098  gsumsub  17108  gsum2dlem2  17131  gsum2dOLD  17133  dprdfsub  17193  dprdfsubOLD  17200  lmhmvsca  17823  psrass1lem  18161  psrlinv  18182  psrcom  18196  evlslem2  18312  coe1fval3  18379  psropprmul  18411  coe1z  18436  coe1mul2  18442  coe1tm  18446  ply1coe  18469  ply1coeOLD  18470  evls1sca  18492  frgpcyg  18722  evpmodpmf1o  18742  mhmvlin  19003  ofco2  19057  mdetleib2  19194  mdetralt  19214  smadiadetlem3  19274  ptrescn  20244  lmcn2  20254  qtopeu  20321  flfcnp2  20612  tgpconcomp  20715  tsmsmhm  20752  tsmssub  20755  tsmsxplem1  20759  negfcncf  21527  pcopt  21626  pcopt2  21627  pi1xfrcnvlem  21660  ovolctb  22005  ovolfs2  22084  uniioombllem2  22096  uniioombllem3  22098  ismbf  22141  mbfconst  22146  ismbfcn2  22150  itg1climres  22225  iblabslem  22338  iblabs  22339  bddmulibl  22349  limccnp  22399  limccnp2  22400  limcco  22401  dvcof  22455  dvcjbr  22456  dvcj  22457  dvfre  22458  dvmptcj  22475  dvmptco  22479  dvcnvlem  22481  dvef  22485  dvlip  22498  dvlipcn  22499  itgsubstlem  22553  plypf1  22713  plyco  22742  dgrcolem1  22774  dgrcolem2  22775  dgrco  22776  plycjlem  22777  taylply2  22867  logcn  23134  leibpi  23408  efrlim  23435  jensenlem2  23453  amgmlem  23455  ftalem7  23488  lgseisenlem4  23763  dchrisum0  23841  cofmpt  27680  ofcfval4  28284  eulerpartgbij  28530  dstfrvclim1  28635  lgamgulmlem2  28797  lgamcvg2  28822  cvmliftlem6  28960  cvmliftphtlem  28987  cvmlift3lem5  28993  elmsubrn  29113  msubco  29116  circum  29265  mblfinlem2  30253  volsupnfl  30260  itgaddnc  30277  itgmulc2nc  30285  ftc1anclem1  30292  ftc1anclem2  30293  ftc1anclem3  30294  ftc1anclem4  30295  ftc1anclem5  30296  ftc1anclem6  30297  ftc1anclem7  30298  ftc1anclem8  30299  fnopabco  30415  upixp  30422  mendassa  31347  cncfcompt  31886  dvcosax  31924  dirkercncflem4  32089  fourierdlem111  32201