Theorem fmptco 5586

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 5037	. 2 |- Rel ( G o. F )
2		funmpt 5161	. . 3 |- Fun ( x e. A |-> T )
3		funrel 5140	. . 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 2139	. . . . . . . . . . . . 13 |- ( x e. A |-> R ) = ( x e. A |-> R )
7	5, 6	fmptd 5574	. . . . . . . . . . . 12 |- ( ph -> ( x e. A |-> R ) : A --> B )
8		fmptco.2	. . . . . . . . . . . . 13 |- ( ph -> F = ( x e. A |-> R ) )
9	8	feq1d 5259	. . . . . . . . . . . 12 |- ( ph -> ( F : A --> B <-> ( x e. A |-> R ) : A --> B ) )
10	7, 9	mpbird 166	. . . . . . . . . . 11 |- ( ph -> F : A --> B )
11		ffun 5275	. . . . . . . . . . 11 |- ( F : A --> B -> Fun F )
12	10, 11	syl 14	. . . . . . . . . 10 |- ( ph -> Fun F )
13		funbrfv 5460	. . . . . . . . . . 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 281	. . . . . . . . 9 |- ( ( ph /\ z F u ) -> ( F ` z ) = u )
16	15	eqcomd 2145	. . . . . . . 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 360	. . . . . 6 |- ( ph -> ( ( z F u /\ u G w ) -> u = ( F ` z ) ) )
19	18	pm4.71rd 391	. . . . 5 |- ( ph -> ( ( z F u /\ u G w ) <-> ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
20	19	exbidv 1797	. . . 4 |- ( ph -> ( E. u ( z F u /\ u G w ) <-> E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) ) )
21		exsimpl 1596	. . . . . . 7 |- ( E. u ( u = ( F ` z ) /\ ( z F u /\ u G w ) ) -> E. u u = ( F ` z ) )
22		isset 2692	. . . . . . 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 274	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> Fun F )
26		fdm 5278	. . . . . . . . . . 11 |- ( F : A --> B -> dom F = A )
27	10, 26	syl 14	. . . . . . . . . 10 |- ( ph -> dom F = A )
28	27	eleq2d 2209	. . . . . . . . 9 |- ( ph -> ( z e. dom F <-> z e. A ) )
29	28	biimpar 295	. . . . . . . 8 |- ( ( ph /\ z e. A ) -> z e. dom F )
30		funfvex 5438	. . . . . . . 8 |- ( ( Fun F /\ z e. dom F ) -> ( F ` z ) e. _V )
31	25, 29, 30	syl2anc 408	. . . . . . 7 |- ( ( ph /\ z e. A ) -> ( F ` z ) e. _V )
32	31	adantrr 470	. . . . . 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 3933	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( z F u <-> z F ( F ` z ) ) )
35		breq1 3932	. . . . . . . . 9 |- ( u = ( F ` z ) -> ( u G w <-> ( F ` z ) G w ) )
36	34, 35	anbi12d 464	. . . . . . . 8 |- ( u = ( F ` z ) -> ( ( z F u /\ u G w ) <-> ( z F ( F ` z ) /\ ( F ` z ) G w ) ) )
37	36	ceqsexgv 2814	. . . . . . 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 5533	. . . . . . . . . . 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 5423	. . . . . . . . . 10 |- ( ph -> ( F ` z ) = ( ( x e. A |-> R ) ` z ) )
42		fmptco.3	. . . . . . . . . 10 |- ( ph -> G = ( y e. B |-> S ) )
43		eqidd 2140	. . . . . . . . . 10 |- ( ph -> w = w )
44	41, 42, 43	breq123d 3943	. . . . . . . . 9 |- ( ph -> ( ( F ` z ) G w <-> ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w ) )
45	40, 44	anbi12d 464	. . . . . . . 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 2281	. . . . . . . . . . 11 |- F/_ x z
47		nfv 1508	. . . . . . . . . . . 12 |- F/ x ph
48		nffvmpt1 5432	. . . . . . . . . . . . . 14 |- F/_ x ( ( x e. A |-> R ) ` z )
49		nfcv 2281	. . . . . . . . . . . . . 14 |- F/_ x ( y e. B |-> S )
50		nfcv 2281	. . . . . . . . . . . . . 14 |- F/_ x w
51	48, 49, 50	nfbr 3974	. . . . . . . . . . . . 13 |- F/ x ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w
52		nfcsb1v 3035	. . . . . . . . . . . . . 14 |- F/_ x [_ z / x ]_ T
53	52	nfeq2 2293	. . . . . . . . . . . . 13 |- F/ x w = [_ z / x ]_ T
54	51, 53	nfbi 1568	. . . . . . . . . . . 12 |- F/ x ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T )
55	47, 54	nfim 1551	. . . . . . . . . . 11 |- F/ x ( ph -> ( ( ( x e. A |-> R ) ` z ) ( y e. B |-> S ) w <-> w = [_ z / x ]_ T ) )
56		fveq2 5421	. . . . . . . . . . . . . 14 |- ( x = z -> ( ( x e. A |-> R ) ` x ) = ( ( x e. A |-> R ) ` z ) )
57	56	breq1d 3939	. . . . . . . . . . . . 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 3012	. . . . . . . . . . . . . 14 |- ( x = z -> T = [_ z / x ]_ T )
59	58	eqeq2d 2151	. . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . 14 |- w e. _V
63		simpl 108	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> y = R )
64	63	eleq1d 2208	. . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . . 17 |- ( ( y = R /\ u = w ) -> S = T )
68	65, 67	eqeq12d 2154	. . . . . . . . . . . . . . . 16 |- ( ( y = R /\ u = w ) -> ( u = S <-> w = T ) )
69	64, 68	anbi12d 464	. . . . . . . . . . . . . . 15 |- ( ( y = R /\ u = w ) -> ( ( y e. B /\ u = S ) <-> ( R e. B /\ w = T ) ) )
70		df-mpt 3991	. . . . . . . . . . . . . . 15 |- ( y e. B |-> S ) = { <. y , u >. | ( y e. B /\ u = S ) }
71	69, 70	brabga 4186	. . . . . . . . . . . . . 14 |- ( ( R e. B /\ w e. _V ) -> ( R ( y e. B |-> S ) w <-> ( R e. B /\ w = T ) ) )
72	5, 62, 71	sylancl 409	. . . . . . . . . . . . 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 5504	. . . . . . . . . . . . . . 15 |- ( ( x e. A /\ R e. B ) -> ( ( x e. A |-> R ) ` x ) = R )
75	73, 5, 74	syl2anc 408	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
76	75	breq1d 3939	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( y e. B |-> S ) w <-> R ( y e. B |-> S ) w ) )
77	5	biantrurd 303	. . . . . . . . . . . . 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 2751	. . . . . . . . . 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 447	. . . . . . . 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 458	. . . . . 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 694	. . . 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 2689	. . . 4 |- z e. _V
89	88, 62	opelco 4711	. . 3 |- ( <. z , w >. e. ( G o. F ) <-> E. u ( z F u /\ u G w ) )
90		df-mpt 3991	. . . . 5 |- ( x e. A |-> T ) = { <. x , v >. | ( x e. A /\ v = T ) }
91	90	eleq2i 2206	. . . 4 |- ( <. z , w >. e. ( x e. A |-> T ) <-> <. z , w >. e. { <. x , v >. | ( x e. A /\ v = T ) } )
92		nfv 1508	. . . . . 6 |- F/ x z e. A
93	52	nfeq2 2293	. . . . . 6 |- F/ x v = [_ z / x ]_ T
94	92, 93	nfan 1544	. . . . 5 |- F/ x ( z e. A /\ v = [_ z / x ]_ T )
95		nfv 1508	. . . . 5 |- F/ v ( z e. A /\ w = [_ z / x ]_ T )
96		eleq1 2202	. . . . . 6 |- ( x = z -> ( x e. A <-> z e. A ) )
97	58	eqeq2d 2151	. . . . . 6 |- ( x = z -> ( v = T <-> v = [_ z / x ]_ T ) )
98	96, 97	anbi12d 464	. . . . 5 |- ( x = z -> ( ( x e. A /\ v = T ) <-> ( z e. A /\ v = [_ z / x ]_ T ) ) )
99		eqeq1 2146	. . . . . 6 |- ( v = w -> ( v = [_ z / x ]_ T <-> w = [_ z / x ]_ T ) )
100	99	anbi2d 459	. . . . 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 4196	. . . 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 4635	1 |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1331   E.wex 1468   e. wcel 1480   _Vcvv 2686   [_csb 3003   <.cop 3530   class class class wbr 3929   {copab 3988   |-> cmpt 3989   dom cdm 4539   o. ccom 4543   Rel wrel 4544   Fun wfun 5117   -->wf 5119   ` cfv 5123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-fv 5131

This theorem is referenced by:  fmptcof  5587  cofmpt  5589  fcompt  5590  fcoconst  5591  ofco  6000  lmcn2  12449  cdivcncfap  12756  negfcncf  12758  dvcj  12842  dvfre  12843