Theorem fmptco 5843

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 5261	. 2 |- Rel ( G o. F )
2		funmpt 5390	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5369	. . 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 2232	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 5831	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5495	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 167	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5511	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 14	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5713	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
14	13	imp 124	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
15	12, 14	sylan 283	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2238	. . . . . . . 8 |- ( ( ph /\ z F u ) -> u = ( F ` z ) )
17	16	a1d 22	. . . . . . 7 |- ( ( ph /\ z F u ) -> ( u G w -> u = ( F ` z ) ) )
18	17	expimpd 363	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 394	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1874	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		exsimpl 1666	. . . . . . 7 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> E. u u = ( F ` z ) )
22		isset 2820	. . . . . . 7 |- ( ( F ` z ) e. _V <-> E. u u = ( F ` z ) )
23	21, 22	sylibr 134	. . . . . 6 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> ( F ` z ) e. _V )
24	23	a1i 9	. . . . 5 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> ( F ` z ) e. _V ) )
25	12	adantr 276	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> Fun F )
26		fdm 5514	. . . . . . . . . . 11 |- ( F : A --> B -> dom F = A )
27	10, 26	syl 14	. . . . . . . . . 10 |- ( ph -> dom F = A )
28	27	eleq2d 2302	. . . . . . . . 9 |- ( ph -> ( z e. dom F <-> z e. A ) )
29	28	biimpar 297	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> z e. dom F )
30		funfvex 5687	. . . . . . . 8 |- ( ( Fun F /\ z e. dom F ) -> ( F ` z ) e. _V )
31	25, 29, 30	syl2anc 411	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( F ` z ) e. _V )
32	31	adantrr 479	. . . . . 6 |- ( ( ph /\ ( z e. A /\ w = [_ z / x ]_ T ) ) -> ( F ` z ) e. _V )
33	32	ex 115	. . . . 5 |- ( ph -> ( ( z e. A /\ w = [_ z / x ]_ T ) -> ( F ` z ) e. _V ) )
34		breq2 4113	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
35		breq1 4112	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
36	34, 35	anbi12d 473	. . . . . . . 8 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
37	36	ceqsexgv 2946	. . . . . . 7 |- ( ( F ` z ) e. _V -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
38		funfvbrb 5791	. . . . . . . . . . 11 |- ( Fun F -> ( z e. dom F <-> z F ( F ` z ) ) )
39	12, 38	syl 14	. . . . . . . . . 10 |- ( ph -> ( z e. dom F <-> z F ( F ` z ) ) )
40	39, 28	bitr3d 190	. . . . . . . . 9 |- ( ph -> ( z F ( F ` z ) <-> z e. A ) )
41	8	fveq1d 5672	. . . . . . . . . 10 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
42		fmptco.3	. . . . . . . . . 10 |- ( ph -> G = ( y e. B |-> S ) )
43		eqidd 2233	. . . . . . . . . 10 |- ( ph -> w = w )
44	41, 42, 43	breq123d 4123	. . . . . . . . 9 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
45	40, 44	anbi12d 473	. . . . . . . 8 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) ) )
46		nfcv 2384	. . . . . . . . . . 11 |- F/_ x z
47		nfv 1577	. . . . . . . . . . . 12 |- F/ x ph
48		nffvmpt1 5681	. . . . . . . . . . . . . 14 |- F/_ x ( ( x e. A |-> R ) ` z )
49		nfcv 2384	. . . . . . . . . . . . . 14 |- F/_ x ( y e. B |-> S )
50		nfcv 2384	. . . . . . . . . . . . . 14 |- F/_ x w
51	48, 49, 50	nfbr 4156	. . . . . . . . . . . . 13 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
52		nfcsb1v 3171	. . . . . . . . . . . . . 14 |- F/_ x [_ z / x ]_ T
53	52	nfeq2 2396	. . . . . . . . . . . . 13 |- F/ x w = [_ z / x ]_ T
54	51, 53	nfbi 1638	. . . . . . . . . . . 12 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
55	47, 54	nfim 1621	. . . . . . . . . . 11 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
56		fveq2 5670	. . . . . . . . . . . . . 14 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
57	56	breq1d 4119	. . . . . . . . . . . . 13 |- ( x = z -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
58		csbeq1a 3147	. . . . . . . . . . . . . 14 |- ( x = z -> T = [_ z / x ]_ T )
59	58	eqeq2d 2244	. . . . . . . . . . . . 13 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
60	57, 59	bibi12d 235	. . . . . . . . . . . 12 |- ( 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 ) ) )
61	60	imbi2d 230	. . . . . . . . . . 11 |- ( 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 ) ) ) )
62		vex 2816	. . . . . . . . . . . . . 14 |- w e. _V
63		simpl 109	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> y = R )
64	63	eleq1d 2301	. . . . . . . . . . . . . . . 16 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
65		simpr 110	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> u = w )
66		fmptco.4	. . . . . . . . . . . . . . . . . 18 |- ( y = R -> S = T )
67	66	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> S = T )
68	65, 67	eqeq12d 2247	. . . . . . . . . . . . . . . 16 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
69	64, 68	anbi12d 473	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
70		df-mpt 4173	. . . . . . . . . . . . . . 15 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
71	69, 70	brabga 4382	. . . . . . . . . . . . . 14 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
72	5, 62, 71	sylancl 413	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
73		simpr 110	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A ) -> x e. A )
74	6	fvmpt2 5761	. . . . . . . . . . . . . . 15 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
75	73, 5, 74	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
76	75	breq1d 4119	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
77	5	biantrurd 305	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
78	72, 76, 77	3bitr4d 220	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
79	78	expcom 116	. . . . . . . . . . 11 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
80	46, 55, 61, 79	vtoclgaf 2880	. . . . . . . . . 10 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
81	80	impcom 125	. . . . . . . . 9 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
82	81	pm5.32da 452	. . . . . . . 8 |- ( ph -> ( ( z e. A /\ ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
83	45, 82	bitrd 188	. . . . . . 7 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
84	37, 83	sylan9bbr 463	. . . . . 6 |- ( ( ph /\ ( F ` z ) e. _V ) -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
85	84	ex 115	. . . . 5 |- ( ph -> ( ( F ` z ) e. _V -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) ) )
86	24, 33, 85	pm5.21ndd 713	. . . 4 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
87	20, 86	bitrd 188	. . 3 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
88		vex 2816	. . . 4 |- z e. _V
89	88, 62	opelco 4927	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
90		df-mpt 4173	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
91	90	eleq2i 2299	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
92		nfv 1577	. . . . . 6 |- F/ x z e. A
93	52	nfeq2 2396	. . . . . 6 |- F/ x v = [_ z / x ]_ T
94	92, 93	nfan 1614	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
95		nfv 1577	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
96		eleq1 2295	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
97	58	eqeq2d 2244	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
98	96, 97	anbi12d 473	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
99		eqeq1 2239	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
100	99	anbi2d 464	. . . . 5 |- ( v = w -> ( ( z e. A /\ v = [_ z / x ]_ T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
101	94, 95, 88, 62, 98, 100	opelopabf 4393	. . . 4 |- ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
102	91, 101	bitri 184	. . 3 |- ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
103	87, 89, 102	3bitr4g 223	. 2 |- ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
104	1, 4, 103	eqrelrdv 4846	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   E.wex 1541   e. wcel 2203   _Vcvv 2813   [_csb 3138   <.cop 3692   class class class wbr 4109   {copab 4170   |-> cmpt 4171   dom cdm 4749   o. ccom 4753   Rel wrel 4754   Fun wfun 5346   -->wf 5348   ` cfv 5352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-fv 5360

This theorem is referenced by:  fmptcof  5844  cofmpt  5846  fcompt  5847  fcoconst  5848  ofco  6285  prdsidlem  13660  pws0g  13664  pwsinvg  13825  pwssub  13826  gsumfzmhm2  14061  psrlinv  14839  lmcn2  15145  cdivcncfap  15469  negfcncf  15471  dvcj  15574  dvfre  15575  dvmptcjx  15589  plyco  15624  plycjlemc  15625