Theorem fmptco 6396

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 5633	. 2 |- Rel ( G o. F )
2		mptrel 5248	. 2 |- Rel ( x e. A |-> T )
3		fmptco.2	. . . . . . . . . . . 12 |- ( ph -> F = ( x e. A |-> R ) )
4		fmptco.1	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> R e. B )
5	3, 4	fmpt3d 6386	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
6	5	ffund 6049	. . . . . . . . . 10 |- ( ph -> Fun F )
7		funbrfv 6234	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
8	7	imp 445	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
9	6, 8	sylan 488	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
10	9	eqcomd 2628	. . . . . . . 8 |- ( ( ph /\ z F u ) -> u = ( F ` z ) )
11	10	a1d 25	. . . . . . 7 |- ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
12	11	expimpd 629	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
13	12	pm4.71rd 667	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
14	13	exbidv 1850	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
15		fvex 6201	. . . . . 6 |- ( F ` z ) e. _V
16		breq2 4657	. . . . . . 7 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
17		breq1 4656	. . . . . . 7 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
18	16, 17	anbi12d 747	. . . . . 6 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
19	15, 18	ceqsexv 3242	. . . . 5 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) )
20		funfvbrb 6330	. . . . . . . . 9 |- ( Fun F -> ( z e. dom F <-> z F ( F ` z ) ) )
21	6, 20	syl 17	. . . . . . . 8 |- ( ph -> ( z e. dom F <-> z F ( F ` z ) ) )
22		fdm 6051	. . . . . . . . . 10 |- ( F : A --> B -> dom F = A )
23	5, 22	syl 17	. . . . . . . . 9 |- ( ph -> dom F = A )
24	23	eleq2d 2687	. . . . . . . 8 |- ( ph -> ( z e. dom F <-> z e. A ) )
25	21, 24	bitr3d 270	. . . . . . 7 |- ( ph -> ( z F ( F ` z ) <-> z e. A ) )
26	3	fveq1d 6193	. . . . . . . 8 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
27		fmptco.3	. . . . . . . 8 |- ( ph -> G = ( y e. B |-> S ) )
28		eqidd 2623	. . . . . . . 8 |- ( ph -> w = w )
29	26, 27, 28	breq123d 4667	. . . . . . 7 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
30	25, 29	anbi12d 747	. . . . . 6 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) ) )
31		nfcv 2764	. . . . . . . . 9 |- F/_ x z
32		nfv 1843	. . . . . . . . . 10 |- F/ x ph
33		nffvmpt1 6199	. . . . . . . . . . . 12 |- F/_ x ( ( x e. A |-> R ) ` z )
34		nfcv 2764	. . . . . . . . . . . 12 |- F/_ x ( y e. B |-> S )
35		nfcv 2764	. . . . . . . . . . . 12 |- F/_ x w
36	33, 34, 35	nfbr 4699	. . . . . . . . . . 11 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
37		nfcsb1v 3549	. . . . . . . . . . . 12 |- F/_ x [_ z / x ]_ T
38	37	nfeq2 2780	. . . . . . . . . . 11 |- F/ x w = [_ z / x ]_ T
39	36, 38	nfbi 1833	. . . . . . . . . 10 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
40	32, 39	nfim 1825	. . . . . . . . 9 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
41		fveq2 6191	. . . . . . . . . . . 12 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
42	41	breq1d 4663	. . . . . . . . . . 11 |- ( x = z -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
43		csbeq1a 3542	. . . . . . . . . . . 12 |- ( x = z -> T = [_ z / x ]_ T )
44	43	eqeq2d 2632	. . . . . . . . . . 11 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
45	42, 44	bibi12d 335	. . . . . . . . . 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 ) ) )
46	45	imbi2d 330	. . . . . . . . 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 ) ) ) )
47		vex 3203	. . . . . . . . . . . 12 |- w e. _V
48		simpl 473	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> y = R )
49	48	eleq1d 2686	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
50		id 22	. . . . . . . . . . . . . . 15 |- ( u = w -> u = w )
51		fmptco.4	. . . . . . . . . . . . . . 15 |- ( y = R -> S = T )
52	50, 51	eqeqan12rd 2640	. . . . . . . . . . . . . 14 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
53	49, 52	anbi12d 747	. . . . . . . . . . . . 13 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
54		df-mpt 4730	. . . . . . . . . . . . 13 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
55	53, 54	brabga 4989	. . . . . . . . . . . 12 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
56	4, 47, 55	sylancl 694	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
57		id 22	. . . . . . . . . . . . 13 |- ( x e. A -> x e. A )
58		eqid 2622	. . . . . . . . . . . . . 14 |- ( x e. A |-> R ) = ( x e. A |-> R )
59	58	fvmpt2 6291	. . . . . . . . . . . . 13 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
60	57, 4, 59	syl2an2 875	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
61	60	breq1d 4663	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
62	4	biantrurd 529	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
63	56, 61, 62	3bitr4d 300	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
64	63	expcom 451	. . . . . . . . 9 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
65	31, 40, 46, 64	vtoclgaf 3271	. . . . . . . 8 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
66	65	impcom 446	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
67	66	pm5.32da 673	. . . . . 6 |- ( ph -> ( ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
68	30, 67	bitrd 268	. . . . 5 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
69	19, 68	syl5bb 272	. . . 4 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
70	14, 69	bitrd 268	. . 3 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
71		vex 3203	. . . 4 |- z e. _V
72	71, 47	opelco 5293	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
73		df-mpt 4730	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
74	73	eleq2i 2693	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
75		nfv 1843	. . . . . 6 |- F/ x z e. A
76	37	nfeq2 2780	. . . . . 6 |- F/ x v = [_ z / x ]_ T
77	75, 76	nfan 1828	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
78		nfv 1843	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
79		eleq1 2689	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
80	43	eqeq2d 2632	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
81	79, 80	anbi12d 747	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
82		eqeq1 2626	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
83	82	anbi2d 740	. . . . 5 |- ( v = w -> ( ( z e. A /\ v = [_ z / x ]_ T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
84	77, 78, 71, 47, 81, 83	opelopabf 5000	. . . 4 |- ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
85	74, 84	bitri 264	. . 3 |- ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
86	70, 72, 85	3bitr4g 303	. 2 |- ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
87	1, 2, 86	eqrelrdv 5216	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   [_csb 3533   <.cop 4183   class class class wbr 4653   {copab 4712   |-> cmpt 4729   dom cdm 5114   o. ccom 5118   Fun wfun 5882   -->wf 5884   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  fmptcof  6397  cofmpt  6399  fcompt  6400  fcoconst  6401  ofco  6917  ccatco  13581  lo1o12  14264  rlimcn1  14319  rlimcn1b  14320  rlimdiv  14376  ackbijnn  14560  setcepi  16738  prf1st  16844  prf2nd  16845  hofcllem  16898  prdsidlem  17322  pws0g  17326  pwsco1mhm  17370  pwsco2mhm  17371  pwsinvg  17528  pwssub  17529  galactghm  17823  efginvrel1  18141  frgpup3lem  18190  gsumzf1o  18313  gsumconst  18334  gsummptshft  18336  gsumzmhm  18337  gsummhm2  18339  gsummptmhm  18340  gsumsub  18348  gsum2dlem2  18370  dprdfsub  18420  lmhmvsca  19045  psrass1lem  19377  psrlinv  19397  psrcom  19409  evlslem2  19512  coe1fval3  19578  psropprmul  19608  coe1z  19633  coe1mul2  19639  coe1tm  19643  ply1coe  19666  evls1sca  19688  frgpcyg  19922  evpmodpmf1o  19942  mhmvlin  20203  ofco2  20257  mdetleib2  20394  mdetralt  20414  smadiadetlem3  20474  ptrescn  21442  lmcn2  21452  qtopeu  21519  flfcnp2  21811  tgpconncomp  21916  tsmsmhm  21949  tsmssub  21952  tsmsxplem1  21956  negfcncf  22722  pcopt  22822  pcopt2  22823  pi1xfrcnvlem  22856  ovolctb  23258  ovolfs2  23339  uniioombllem2  23351  uniioombllem3  23353  ismbf  23397  mbfconst  23402  ismbfcn2  23406  itg1climres  23481  iblabslem  23594  iblabs  23595  bddmulibl  23605  limccnp  23655  limccnp2  23656  limcco  23657  dvcof  23711  dvcjbr  23712  dvcj  23713  dvfre  23714  dvmptcj  23731  dvmptco  23735  dvcnvlem  23739  dvef  23743  dvlip  23756  dvlipcn  23757  itgsubstlem  23811  plypf1  23968  plyco  23997  dgrcolem1  24029  dgrcolem2  24030  dgrco  24031  plycjlem  24032  taylply2  24122  logcn  24393  leibpi  24669  efrlim  24696  jensenlem2  24714  amgmlem  24716  lgamgulmlem2  24756  lgamcvg2  24781  ftalem7  24805  lgseisenlem4  25103  dchrisum0  25209  ofcfval4  30167  eulerpartgbij  30434  dstfrvclim1  30539  cvmliftlem6  31272  cvmliftphtlem  31299  cvmlift3lem5  31305  elmsubrn  31425  msubco  31428  circum  31568  mblfinlem2  33447  volsupnfl  33454  itgaddnc  33470  itgmulc2nc  33478  ftc1anclem1  33485  ftc1anclem2  33486  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  fnopabco  33517  upixp  33524  mendassa  37764  fsovrfovd  38303  fsovcnvlem  38307  cncfcompt  40096  dvcosax  40141  dirkercncflem4  40323  fourierdlem111  40434  meadjiunlem  40682  meadjiun  40683  amgmwlem  42548  amgmlemALT  42549