Theorem fmptco 6064

Description: Composition of two functions expressed as ordered-pair class abstractions. If has the equation and the equation then has the equation . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)

Hypotheses

Ref	Expression
fmptco.1
fmptco.2
fmptco.3
fmptco.4

Assertion

Ref	Expression
fmptco

Distinct variable groups:   ,   ,,   ,   ,   ,S   ,

Proof of Theorem fmptco

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 5510	. 2
2		funmpt 5629	. . 3
3		funrel 5610	. . 3
4	2, 3	ax-mp 5	. 2
5		fmptco.1	. . . . . . . . . . . . 13
6		eqid 2457	. . . . . . . . . . . . 13
7	5, 6	fmptd 6055	. . . . . . . . . . . 12
8		fmptco.2	. . . . . . . . . . . . 13
9	8	feq1d 5722	. . . . . . . . . . . 12
10	7, 9	mpbird 232	. . . . . . . . . . 11
11		ffun 5738	. . . . . . . . . . 11
12	10, 11	syl 16	. . . . . . . . . 10
13		funbrfv 5911	. . . . . . . . . . 11
14	13	imp 429	. . . . . . . . . 10
15	12, 14	sylan 471	. . . . . . . . 9
16	15	eqcomd 2465	. . . . . . . 8
17	16	a1d 25	. . . . . . 7
18	17	expimpd 603	. . . . . 6
19	18	pm4.71rd 635	. . . . 5
20	19	exbidv 1714	. . . 4
21		fvex 5881	. . . . . 6
22		breq2 4456	. . . . . . 7
23		breq1 4455	. . . . . . 7
24	22, 23	anbi12d 710	. . . . . 6
25	21, 24	ceqsexv 3146	. . . . 5
26		funfvbrb 6000	. . . . . . . . 9
27	12, 26	syl 16	. . . . . . . 8
28		fdm 5740	. . . . . . . . . 10
29	10, 28	syl 16	. . . . . . . . 9
30	29	eleq2d 2527	. . . . . . . 8
31	27, 30	bitr3d 255	. . . . . . 7
32	8	fveq1d 5873	. . . . . . . 8
33		fmptco.3	. . . . . . . 8
34		eqidd 2458	. . . . . . . 8
35	32, 33, 34	breq123d 4466	. . . . . . 7
36	31, 35	anbi12d 710	. . . . . 6
37		nfcv 2619	. . . . . . . . 9
38		nfv 1707	. . . . . . . . . 10
39		nffvmpt1 5879	. . . . . . . . . . . 12
40		nfcv 2619	. . . . . . . . . . . 12
41		nfcv 2619	. . . . . . . . . . . 12
42	39, 40, 41	nfbr 4496	. . . . . . . . . . 11
43		nfcsb1v 3450	. . . . . . . . . . . 12
44	43	nfeq2 2636	. . . . . . . . . . 11
45	42, 44	nfbi 1934	. . . . . . . . . 10
46	38, 45	nfim 1920	. . . . . . . . 9
47		fveq2 5871	. . . . . . . . . . . 12
48	47	breq1d 4462	. . . . . . . . . . 11
49		csbeq1a 3443	. . . . . . . . . . . 12
50	49	eqeq2d 2471	. . . . . . . . . . 11
51	48, 50	bibi12d 321	. . . . . . . . . 10
52	51	imbi2d 316	. . . . . . . . 9
53		vex 3112	. . . . . . . . . . . 12
54		simpl 457	. . . . . . . . . . . . . . 15
55	54	eleq1d 2526	. . . . . . . . . . . . . 14
56		simpr 461	. . . . . . . . . . . . . . 15
57		fmptco.4	. . . . . . . . . . . . . . . 16
58	57	adantr 465	. . . . . . . . . . . . . . 15
59	56, 58	eqeq12d 2479	. . . . . . . . . . . . . 14
60	55, 59	anbi12d 710	. . . . . . . . . . . . 13
61		df-mpt 4512	. . . . . . . . . . . . 13
62	60, 61	brabga 4766	. . . . . . . . . . . 12
63	5, 53, 62	sylancl 662	. . . . . . . . . . 11
64		simpr 461	. . . . . . . . . . . . 13
65	6	fvmpt2 5963	. . . . . . . . . . . . 13
66	64, 5, 65	syl2anc 661	. . . . . . . . . . . 12
67	66	breq1d 4462	. . . . . . . . . . 11
68	5	biantrurd 508	. . . . . . . . . . 11
69	63, 67, 68	3bitr4d 285	. . . . . . . . . 10
70	69	expcom 435	. . . . . . . . 9
71	37, 46, 52, 70	vtoclgaf 3172	. . . . . . . 8
72	71	impcom 430	. . . . . . 7
73	72	pm5.32da 641	. . . . . 6
74	36, 73	bitrd 253	. . . . 5
75	25, 74	syl5bb 257	. . . 4
76	20, 75	bitrd 253	. . 3
77		vex 3112	. . . 4
78	77, 53	opelco 5179	. . 3
79		df-mpt 4512	. . . . 5
80	79	eleq2i 2535	. . . 4
81		nfv 1707	. . . . . 6
82	43	nfeq2 2636	. . . . . 6
83	81, 82	nfan 1928	. . . . 5
84		nfv 1707	. . . . 5
85		eleq1 2529	. . . . . 6
86	49	eqeq2d 2471	. . . . . 6
87	85, 86	anbi12d 710	. . . . 5
88		eqeq1 2461	. . . . . 6
89	88	anbi2d 703	. . . . 5
90	83, 84, 77, 53, 87, 89	opelopabf 4777	. . . 4
91	80, 90	bitri 249	. . 3
92	76, 78, 91	3bitr4g 288	. 2
93	1, 4, 92	eqrelrdv 5104	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  cvv 3109  [_csb 3434  <.cop 4035   class class class wbr 4452  {copab 4509  e.cmpt 4510  domcdm 5004  o.ccom 5008  Relwrel 5009  Funwfun 5587  -->wf 5589  `cfv 5593

This theorem is referenced by:  fmptcof  6065  fcompt  6067  fcoconst  6068  ofco  6560  ccatco  12801  lo1o12  13356  rlimcn1  13411  rlimcn1b  13412  rlimdiv  13468  ackbijnn  13640  setcepi  15415  prf1st  15473  prf2nd  15474  hofcllem  15527  prdsidlem  15952  pws0g  15956  pwsco1mhm  16001  pwsco2mhm  16002  pwsinvg  16182  pwssub  16183  galactghm  16428  efginvrel1  16746  frgpup3lem  16795  gsumzf1o  16917  gsumzf1oOLD  16920  gsumconst  16954  gsummptshft  16956  gsumzmhm  16957  gsumzmhmOLD  16958  gsummhm2  16961  gsummhm2OLD  16962  gsummptmhm  16963  gsumsub  16974  gsumsubOLD  16975  gsum2dlem2  16998  gsum2dOLD  17000  dprdfsub  17061  dprdfsubOLD  17068  lmhmvsca  17691  psrass1lem  18029  psrlinv  18050  psrcom  18064  evlslem2  18180  coe1fval3  18247  psropprmul  18279  coe1z  18304  coe1mul2  18310  coe1tm  18314  ply1coe  18337  ply1coeOLD  18338  evls1sca  18360  frgpcyg  18612  evpmodpmf1o  18632  mhmvlin  18899  ofco2  18953  mdetleib2  19090  mdetralt  19110  smadiadetlem3  19170  ptrescn  20140  lmcn2  20150  qtopeu  20217  flfcnp2  20508  tgpconcomp  20611  tsmsmhm  20648  tsmssub  20651  tsmsxplem1  20655  negfcncf  21423  pcopt  21522  pcopt2  21523  pi1xfrcnvlem  21556  ovolctb  21901  ovolfs2  21980  uniioombllem2  21992  uniioombllem3  21994  ismbf  22037  mbfconst  22042  ismbfcn2  22046  itg1climres  22121  iblabslem  22234  iblabs  22235  bddmulibl  22245  limccnp  22295  limccnp2  22296  limcco  22297  dvcof  22351  dvcjbr  22352  dvcj  22353  dvfre  22354  dvmptcj  22371  dvmptco  22375  dvcnvlem  22377  dvef  22381  dvlip  22394  dvlipcn  22395  itgsubstlem  22449  plypf1  22609  plyco  22638  dgrcolem1  22670  dgrcolem2  22671  dgrco  22672  plycjlem  22673  taylply2  22763  logcn  23028  leibpi  23273  efrlim  23299  jensenlem2  23317  amgmlem  23319  ftalem7  23352  lgseisenlem4  23627  dchrisum0  23705  cofmpt  27504  ofcfval4  28104  eulerpartgbij  28311  dstfrvclim1  28416  lgamgulmlem2  28572  lgamcvg2  28597  cvmliftlem6  28735  cvmliftphtlem  28762  cvmlift3lem5  28768  elmsubrn  28888  msubco  28891  circum  29040  mblfinlem2  30052  volsupnfl  30059  itgaddnc  30075  itgmulc2nc  30083  ftc1anclem1  30090  ftc1anclem2  30091  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  fnopabco  30213  upixp  30220  mendassa  31143  cncfcompt  31685  dvcosax  31723  dirkercncflem4  31888  fourierdlem111  32000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601