Theorem fmptco 5478

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 4942	. 2 |- Rel ( G o. F )
2		funmpt 5065	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5045	. . 3 |- ( Fun ( x e. A |-> T ) -> Rel ( x e. A |-> T ) )
4	2, 3	ax-mp 7	. 2 |- Rel ( x e. A |-> T )
5		fmptco.1	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> R e. B )
6		eqid 2089	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 5466	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5162	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 166	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5177	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 14	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5356	. . . . . . . . . . 11 |- ( Fun F -> ( z F u -> ( F ` z ) = u ) )
14	13	imp 123	. . . . . . . . . 10 |- ( ( Fun F /\ z F u ) -> ( F ` z ) = u )
15	12, 14	sylan 278	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2094	. . . . . . . 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 356	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 387	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1754	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		exsimpl 1554	. . . . . . 7 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> E. u u = ( F ` z ) )
22		isset 2626	. . . . . . 7 |- ( ( F ` z ) e. _V <-> E. u u = ( F ` z ) )
23	21, 22	sylibr 133	. . . . . 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 271	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> Fun F )
26		fdm 5179	. . . . . . . . . . 11 |- ( F : A --> B -> dom F = A )
27	10, 26	syl 14	. . . . . . . . . 10 |- ( ph -> dom F = A )
28	27	eleq2d 2158	. . . . . . . . 9 |- ( ph -> ( z e. dom F <-> z e. A ) )
29	28	biimpar 292	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> z e. dom F )
30		funfvex 5335	. . . . . . . 8 |- ( ( Fun F /\ z e. dom F ) -> ( F ` z ) e. _V )
31	25, 29, 30	syl2anc 404	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( F ` z ) e. _V )
32	31	adantrr 464	. . . . . 6 |- ( ( ph /\ ( z e. A /\ w = [_ z / x ]_ T ) ) -> ( F ` z ) e. _V )
33	32	ex 114	. . . . 5 |- ( ph -> ( ( z e. A /\ w = [_ z / x ]_ T ) -> ( F ` z ) e. _V ) )
34		breq2 3855	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
35		breq1 3854	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
36	34, 35	anbi12d 458	. . . . . . . 8 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
37	36	ceqsexgv 2747	. . . . . . 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 5426	. . . . . . . . . . 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 189	. . . . . . . . 9 |- ( ph -> ( z F ( F ` z ) <-> z e. A ) )
41	8	fveq1d 5320	. . . . . . . . . 10 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
42		fmptco.3	. . . . . . . . . 10 |- ( ph -> G = ( y e. B |-> S ) )
43		eqidd 2090	. . . . . . . . . 10 |- ( ph -> w = w )
44	41, 42, 43	breq123d 3865	. . . . . . . . 9 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
45	40, 44	anbi12d 458	. . . . . . . 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 2229	. . . . . . . . . . 11 |- F/_ x z
47		nfv 1467	. . . . . . . . . . . 12 |- F/ x ph
48		nffvmpt1 5329	. . . . . . . . . . . . . 14 |- F/_ x ( ( x e. A |-> R ) ` z )
49		nfcv 2229	. . . . . . . . . . . . . 14 |- F/_ x ( y e. B |-> S )
50		nfcv 2229	. . . . . . . . . . . . . 14 |- F/_ x w
51	48, 49, 50	nfbr 3895	. . . . . . . . . . . . 13 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
52		nfcsb1v 2964	. . . . . . . . . . . . . 14 |- F/_ x [_ z / x ]_ T
53	52	nfeq2 2241	. . . . . . . . . . . . 13 |- F/ x w = [_ z / x ]_ T
54	51, 53	nfbi 1527	. . . . . . . . . . . 12 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
55	47, 54	nfim 1510	. . . . . . . . . . 11 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
56		fveq2 5318	. . . . . . . . . . . . . 14 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
57	56	breq1d 3861	. . . . . . . . . . . . 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 2942	. . . . . . . . . . . . . 14 |- ( x = z -> T = [_ z / x ]_ T )
59	58	eqeq2d 2100	. . . . . . . . . . . . 13 |- ( x = z -> ( w = T <-> w = [_ z / x ]_ T ) )
60	57, 59	bibi12d 234	. . . . . . . . . . . 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 229	. . . . . . . . . . 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 2623	. . . . . . . . . . . . . 14 |- w e. _V
63		simpl 108	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> y = R )
64	63	eleq1d 2157	. . . . . . . . . . . . . . . 16 |- ( ( y = R /\ u = w ) -> ( y e. B <-> R e. B ) )
65		simpr 109	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> u = w )
66		fmptco.4	. . . . . . . . . . . . . . . . . 18 |- ( y = R -> S = T )
67	66	adantr 271	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> S = T )
68	65, 67	eqeq12d 2103	. . . . . . . . . . . . . . . 16 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
69	64, 68	anbi12d 458	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
70		df-mpt 3907	. . . . . . . . . . . . . . 15 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
71	69, 70	brabga 4100	. . . . . . . . . . . . . 14 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
72	5, 62, 71	sylancl 405	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
73		simpr 109	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A ) -> x e. A )
74	6	fvmpt2 5399	. . . . . . . . . . . . . . 15 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
75	73, 5, 74	syl2anc 404	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
76	75	breq1d 3861	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
77	5	biantrurd 300	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( w = T <-> ( R e. B /\ w = T ) ) )
78	72, 76, 77	3bitr4d 219	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) )
79	78	expcom 115	. . . . . . . . . . 11 |- ( x e. A -> ( ph -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> w = T ) ) )
80	46, 55, 61, 79	vtoclgaf 2685	. . . . . . . . . 10 |- ( z e. A -> ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) ) )
81	80	impcom 124	. . . . . . . . 9 |- ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
82	81	pm5.32da 441	. . . . . . . 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 187	. . . . . . 7 |- ( ph -> ( ( z F ( F ` z ) /\ ( F ` z ) G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
84	37, 83	sylan9bbr 452	. . . . . 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 114	. . . . 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 657	. . . 4 |- ( ph -> ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
87	20, 86	bitrd 187	. . 3 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> ( z e. A /\ w = [_ z / x ]_ T ) ) )
88		vex 2623	. . . 4 |- z e. _V
89	88, 62	opelco 4621	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
90		df-mpt 3907	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
91	90	eleq2i 2155	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
92		nfv 1467	. . . . . 6 |- F/ x z e. A
93	52	nfeq2 2241	. . . . . 6 |- F/ x v = [_ z / x ]_ T
94	92, 93	nfan 1503	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
95		nfv 1467	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
96		eleq1 2151	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
97	58	eqeq2d 2100	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
98	96, 97	anbi12d 458	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
99		eqeq1 2095	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
100	99	anbi2d 453	. . . . 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 4110	. . . 4 |- ( <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } <-> ( z e. A /\ w = [_ z / x ]_ T ) )
102	91, 101	bitri 183	. . 3 |- ( <. z , w >. e. ( x e. A |-> T ) <-> ( z e. A /\ w = [_ z / x ]_ T ) )
103	87, 89, 102	3bitr4g 222	. 2 |- ( ph -> ( <. z , w >. e. ( G o. F ) <-> <. z , w >. e. ( x e. A |-> T ) ) )
104	1, 4, 103	eqrelrdv 4547	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1290   E.wex 1427   e. wcel 1439   _Vcvv 2620   [_csb 2934   <.cop 3453   class class class wbr 3851   {copab 3904   |-> cmpt 3905   dom cdm 4452   o. ccom 4456   Rel wrel 4457   Fun wfun 5022   -->wf 5024   ` cfv 5028

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015  ax-pr 4045

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2622  df-sbc 2842  df-csb 2935  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-opab 3906  df-mpt 3907  df-id 4129  df-xp 4458  df-rel 4459  df-cnv 4460  df-co 4461  df-dm 4462  df-rn 4463  df-res 4464  df-ima 4465  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-fv 5036

This theorem is referenced by:  fmptcof  5479  fcompt  5481  fcoconst  5482  ofco  5887