Theorem mapfien 7609

Description: A bijection of the base sets induces a bijection on the set of finitely supported functions. (Contributed by Mario Carneiro, 30-May-2015.)

Hypotheses

Ref	Expression
mapfien.s	|- S = { x e. ( B ^m A ) | ( `' x " ( _V \ { Z } ) ) e. Fin }
mapfien.t	|- T = { x e. ( D ^m C ) | ( `' x " ( _V \ { W } ) ) e. Fin }
mapfien.w	|- W = ( G ` Z )
mapfien.f	|- ( ph -> F : C -1-1-onto-> A )
mapfien.g	|- ( ph -> G : B -1-1-onto-> D )
mapfien.a	|- ( ph -> A e. _V )
mapfien.b	|- ( ph -> B e. _V )
mapfien.c	|- ( ph -> C e. _V )
mapfien.d	|- ( ph -> D e. _V )
mapfien.z	|- ( ph -> Z e. B )

Assertion

Ref	Expression
mapfien	|- ( ph -> ( f e. S |-> ( G o. ( f o. F ) ) ) : S -1-1-onto-> T )

Distinct variable groups:   x, A   x, B   x, C   x, f, F   f, G, x   ph, f   x, D   S, f   T, f   x, W   x, Z

Allowed substitution hints:   ph( x)   A( f)   B( f)   C( f)   D( f)   S( x)   T( x)   W( f)   Z( f)

Proof of Theorem mapfien

Dummy variable g is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2404	. 2 |- ( f e. S |-> ( G o. ( f o. F ) ) ) = ( f e. S |-> ( G o. ( f o. F ) ) )
2		mapfien.g	. . . . . . 7 |- ( ph -> G : B -1-1-onto-> D )
3		f1of 5633	. . . . . . 7 |- ( G : B -1-1-onto-> D -> G : B --> D )
4	2, 3	syl 16	. . . . . 6 |- ( ph -> G : B --> D )
5	4	adantr 452	. . . . 5 |- ( ( ph /\ f e. S ) -> G : B --> D )
6		cnveq 5005	. . . . . . . . . . . 12 |- ( x = f -> `' x = `' f )
7	6	imaeq1d 5161	. . . . . . . . . . 11 |- ( x = f -> ( `' x " ( _V \ { Z } ) ) = ( `' f " ( _V \ { Z } ) ) )
8	7	eleq1d 2470	. . . . . . . . . 10 |- ( x = f -> ( ( `' x " ( _V \ { Z } ) ) e. Fin <-> ( `' f " ( _V \ { Z } ) ) e. Fin ) )
9		mapfien.s	. . . . . . . . . 10 |- S = { x e. ( B ^m A ) | ( `' x " ( _V \ { Z } ) ) e. Fin }
10	8, 9	elrab2 3054	. . . . . . . . 9 |- ( f e. S <-> ( f e. ( B ^m A ) /\ ( `' f " ( _V \ { Z } ) ) e. Fin ) )
11	10	simplbi 447	. . . . . . . 8 |- ( f e. S -> f e. ( B ^m A ) )
12	11	adantl 453	. . . . . . 7 |- ( ( ph /\ f e. S ) -> f e. ( B ^m A ) )
13		elmapi 6997	. . . . . . 7 |- ( f e. ( B ^m A ) -> f : A --> B )
14	12, 13	syl 16	. . . . . 6 |- ( ( ph /\ f e. S ) -> f : A --> B )
15		mapfien.f	. . . . . . . 8 |- ( ph -> F : C -1-1-onto-> A )
16		f1of 5633	. . . . . . . 8 |- ( F : C -1-1-onto-> A -> F : C --> A )
17	15, 16	syl 16	. . . . . . 7 |- ( ph -> F : C --> A )
18	17	adantr 452	. . . . . 6 |- ( ( ph /\ f e. S ) -> F : C --> A )
19		fco 5559	. . . . . 6 |- ( ( f : A --> B /\ F : C --> A ) -> ( f o. F ) : C --> B )
20	14, 18, 19	syl2anc 643	. . . . 5 |- ( ( ph /\ f e. S ) -> ( f o. F ) : C --> B )
21		fco 5559	. . . . 5 |- ( ( G : B --> D /\ ( f o. F ) : C --> B ) -> ( G o. ( f o. F ) ) : C --> D )
22	5, 20, 21	syl2anc 643	. . . 4 |- ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) : C --> D )
23		mapfien.d	. . . . . 6 |- ( ph -> D e. _V )
24		mapfien.c	. . . . . 6 |- ( ph -> C e. _V )
25		elmapg 6990	. . . . . 6 |- ( ( D e. _V /\ C e. _V ) -> ( ( G o. ( f o. F ) ) e. ( D ^m C ) <-> ( G o. ( f o. F ) ) : C --> D ) )
26	23, 24, 25	syl2anc 643	. . . . 5 |- ( ph -> ( ( G o. ( f o. F ) ) e. ( D ^m C ) <-> ( G o. ( f o. F ) ) : C --> D ) )
27	26	adantr 452	. . . 4 |- ( ( ph /\ f e. S ) -> ( ( G o. ( f o. F ) ) e. ( D ^m C ) <-> ( G o. ( f o. F ) ) : C --> D ) )
28	22, 27	mpbird 224	. . 3 |- ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) e. ( D ^m C ) )
29		cnvco 5015	. . . . . . 7 |- `' ( G o. ( f o. F ) ) = ( `' ( f o. F ) o. `' G )
30	29	imaeq1i 5159	. . . . . 6 |- ( `' ( G o. ( f o. F ) ) " ( _V \ { W } ) ) = ( ( `' ( f o. F ) o. `' G ) " ( _V \ { W } ) )
31		imaco 5334	. . . . . 6 |- ( ( `' ( f o. F ) o. `' G ) " ( _V \ { W } ) ) = ( `' ( f o. F ) " ( `' G " ( _V \ { W } ) ) )
32	30, 31	eqtri 2424	. . . . 5 |- ( `' ( G o. ( f o. F ) ) " ( _V \ { W } ) ) = ( `' ( f o. F ) " ( `' G " ( _V \ { W } ) ) )
33		cnvco 5015	. . . . . 6 |- `' ( f o. F ) = ( `' F o. `' f )
34	33	imaeq1i 5159	. . . . 5 |- ( `' ( f o. F ) " ( `' G " ( _V \ { W } ) ) ) = ( ( `' F o. `' f ) " ( `' G " ( _V \ { W } ) ) )
35		imaco 5334	. . . . 5 |- ( ( `' F o. `' f ) " ( `' G " ( _V \ { W } ) ) ) = ( `' F " ( `' f " ( `' G " ( _V \ { W } ) ) ) )
36	32, 34, 35	3eqtri 2428	. . . 4 |- ( `' ( G o. ( f o. F ) ) " ( _V \ { W } ) ) = ( `' F " ( `' f " ( `' G " ( _V \ { W } ) ) ) )
37	15	adantr 452	. . . . . 6 |- ( ( ph /\ f e. S ) -> F : C -1-1-onto-> A )
38		dff1o3 5639	. . . . . . 7 |- ( F : C -1-1-onto-> A <-> ( F : C -onto-> A /\ Fun `' F ) )
39	38	simprbi 451	. . . . . 6 |- ( F : C -1-1-onto-> A -> Fun `' F )
40	37, 39	syl 16	. . . . 5 |- ( ( ph /\ f e. S ) -> Fun `' F )
41	10	simprbi 451	. . . . . . 7 |- ( f e. S -> ( `' f " ( _V \ { Z } ) ) e. Fin )
42	41	adantl 453	. . . . . 6 |- ( ( ph /\ f e. S ) -> ( `' f " ( _V \ { Z } ) ) e. Fin )
43	2	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ f e. S ) -> G : B -1-1-onto-> D )
44		f1ofun 5635	. . . . . . . . . 10 |- ( G : B -1-1-onto-> D -> Fun G )
45		funcnvcnv 5468	. . . . . . . . . 10 |- ( Fun G -> Fun `' `' G )
46	43, 44, 45	3syl 19	. . . . . . . . 9 |- ( ( ph /\ f e. S ) -> Fun `' `' G )
47		imadif 5487	. . . . . . . . 9 |- ( Fun `' `' G -> ( `' G " ( _V \ { W } ) ) = ( ( `' G " _V ) \ ( `' G " { W } ) ) )
48	46, 47	syl 16	. . . . . . . 8 |- ( ( ph /\ f e. S ) -> ( `' G " ( _V \ { W } ) ) = ( ( `' G " _V ) \ ( `' G " { W } ) ) )
49		ssv 3328	. . . . . . . . . 10 |- ( `' G " _V ) C_ _V
50		ssdif 3442	. . . . . . . . . 10 |- ( ( `' G " _V ) C_ _V -> ( ( `' G " _V ) \ ( `' G " { W } ) ) C_ ( _V \ ( `' G " { W } ) ) )
51	49, 50	ax-mp 8	. . . . . . . . 9 |- ( ( `' G " _V ) \ ( `' G " { W } ) ) C_ ( _V \ ( `' G " { W } ) )
52		mapfien.z	. . . . . . . . . . . . 13 |- ( ph -> Z e. B )
53	52	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ f e. S ) -> Z e. B )
54		mapfien.w	. . . . . . . . . . . . . . 15 |- W = ( G ` Z )
55	54	eqcomi 2408	. . . . . . . . . . . . . 14 |- ( G ` Z ) = W
56		fvex 5701	. . . . . . . . . . . . . . 15 |- ( G ` Z ) e. _V
57	56	elsnc 3797	. . . . . . . . . . . . . 14 |- ( ( G ` Z ) e. { W } <-> ( G ` Z ) = W )
58	55, 57	mpbir 201	. . . . . . . . . . . . 13 |- ( G ` Z ) e. { W }
59	58	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ f e. S ) -> ( G ` Z ) e. { W } )
60		ffn 5550	. . . . . . . . . . . . 13 |- ( G : B --> D -> G Fn B )
61		elpreima 5809	. . . . . . . . . . . . 13 |- ( G Fn B -> ( Z e. ( `' G " { W } ) <-> ( Z e. B /\ ( G ` Z ) e. { W } ) ) )
62	5, 60, 61	3syl 19	. . . . . . . . . . . 12 |- ( ( ph /\ f e. S ) -> ( Z e. ( `' G " { W } ) <-> ( Z e. B /\ ( G ` Z ) e. { W } ) ) )
63	53, 59, 62	mpbir2and 889	. . . . . . . . . . 11 |- ( ( ph /\ f e. S ) -> Z e. ( `' G " { W } ) )
64	63	snssd 3903	. . . . . . . . . 10 |- ( ( ph /\ f e. S ) -> { Z } C_ ( `' G " { W } ) )
65	64	sscond 3444	. . . . . . . . 9 |- ( ( ph /\ f e. S ) -> ( _V \ ( `' G " { W } ) ) C_ ( _V \ { Z } ) )
66	51, 65	syl5ss 3319	. . . . . . . 8 |- ( ( ph /\ f e. S ) -> ( ( `' G " _V ) \ ( `' G " { W } ) ) C_ ( _V \ { Z } ) )
67	48, 66	eqsstrd 3342	. . . . . . 7 |- ( ( ph /\ f e. S ) -> ( `' G " ( _V \ { W } ) ) C_ ( _V \ { Z } ) )
68		imass2 5199	. . . . . . 7 |- ( ( `' G " ( _V \ { W } ) ) C_ ( _V \ { Z } ) -> ( `' f " ( `' G " ( _V \ { W } ) ) ) C_ ( `' f " ( _V \ { Z } ) ) )
69	67, 68	syl 16	. . . . . 6 |- ( ( ph /\ f e. S ) -> ( `' f " ( `' G " ( _V \ { W } ) ) ) C_ ( `' f " ( _V \ { Z } ) ) )
70		ssfi 7288	. . . . . 6 |- ( ( ( `' f " ( _V \ { Z } ) ) e. Fin /\ ( `' f " ( `' G " ( _V \ { W } ) ) ) C_ ( `' f " ( _V \ { Z } ) ) ) -> ( `' f " ( `' G " ( _V \ { W } ) ) ) e. Fin )
71	42, 69, 70	syl2anc 643	. . . . 5 |- ( ( ph /\ f e. S ) -> ( `' f " ( `' G " ( _V \ { W } ) ) ) e. Fin )
72		imafi 7357	. . . . 5 |- ( ( Fun `' F /\ ( `' f " ( `' G " ( _V \ { W } ) ) ) e. Fin ) -> ( `' F " ( `' f " ( `' G " ( _V \ { W } ) ) ) ) e. Fin )
73	40, 71, 72	syl2anc 643	. . . 4 |- ( ( ph /\ f e. S ) -> ( `' F " ( `' f " ( `' G " ( _V \ { W } ) ) ) ) e. Fin )
74	36, 73	syl5eqel 2488	. . 3 |- ( ( ph /\ f e. S ) -> ( `' ( G o. ( f o. F ) ) " ( _V \ { W } ) ) e. Fin )
75		cnveq 5005	. . . . . 6 |- ( x = ( G o. ( f o. F ) ) -> `' x = `' ( G o. ( f o. F ) ) )
76	75	imaeq1d 5161	. . . . 5 |- ( x = ( G o. ( f o. F ) ) -> ( `' x " ( _V \ { W } ) ) = ( `' ( G o. ( f o. F ) ) " ( _V \ { W } ) ) )
77	76	eleq1d 2470	. . . 4 |- ( x = ( G o. ( f o. F ) ) -> ( ( `' x " ( _V \ { W } ) ) e. Fin <-> ( `' ( G o. ( f o. F ) ) " ( _V \ { W } ) ) e. Fin ) )
78		mapfien.t	. . . 4 |- T = { x e. ( D ^m C ) | ( `' x " ( _V \ { W } ) ) e. Fin }
79	77, 78	elrab2 3054	. . 3 |- ( ( G o. ( f o. F ) ) e. T <-> ( ( G o. ( f o. F ) ) e. ( D ^m C ) /\ ( `' ( G o. ( f o. F ) ) " ( _V \ { W } ) ) e. Fin ) )
80	28, 74, 79	sylanbrc 646	. 2 |- ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) e. T )
81		f1ocnv 5646	. . . . . . . 8 |- ( G : B -1-1-onto-> D -> `' G : D -1-1-onto-> B )
82		f1of 5633	. . . . . . . 8 |- ( `' G : D -1-1-onto-> B -> `' G : D --> B )
83	2, 81, 82	3syl 19	. . . . . . 7 |- ( ph -> `' G : D --> B )
84	83	adantr 452	. . . . . 6 |- ( ( ph /\ g e. T ) -> `' G : D --> B )
85		simpr 448	. . . . . . . . 9 |- ( ( ph /\ g e. T ) -> g e. T )
86		cnveq 5005	. . . . . . . . . . . 12 |- ( x = g -> `' x = `' g )
87	86	imaeq1d 5161	. . . . . . . . . . 11 |- ( x = g -> ( `' x " ( _V \ { W } ) ) = ( `' g " ( _V \ { W } ) ) )
88	87	eleq1d 2470	. . . . . . . . . 10 |- ( x = g -> ( ( `' x " ( _V \ { W } ) ) e. Fin <-> ( `' g " ( _V \ { W } ) ) e. Fin ) )
89	88, 78	elrab2 3054	. . . . . . . . 9 |- ( g e. T <-> ( g e. ( D ^m C ) /\ ( `' g " ( _V \ { W } ) ) e. Fin ) )
90	85, 89	sylib 189	. . . . . . . 8 |- ( ( ph /\ g e. T ) -> ( g e. ( D ^m C ) /\ ( `' g " ( _V \ { W } ) ) e. Fin ) )
91	90	simpld 446	. . . . . . 7 |- ( ( ph /\ g e. T ) -> g e. ( D ^m C ) )
92		elmapi 6997	. . . . . . 7 |- ( g e. ( D ^m C ) -> g : C --> D )
93	91, 92	syl 16	. . . . . 6 |- ( ( ph /\ g e. T ) -> g : C --> D )
94		fco 5559	. . . . . 6 |- ( ( `' G : D --> B /\ g : C --> D ) -> ( `' G o. g ) : C --> B )
95	84, 93, 94	syl2anc 643	. . . . 5 |- ( ( ph /\ g e. T ) -> ( `' G o. g ) : C --> B )
96		f1ocnv 5646	. . . . . . 7 |- ( F : C -1-1-onto-> A -> `' F : A -1-1-onto-> C )
97		f1of 5633	. . . . . . 7 |- ( `' F : A -1-1-onto-> C -> `' F : A --> C )
98	15, 96, 97	3syl 19	. . . . . 6 |- ( ph -> `' F : A --> C )
99	98	adantr 452	. . . . 5 |- ( ( ph /\ g e. T ) -> `' F : A --> C )
100		fco 5559	. . . . 5 |- ( ( ( `' G o. g ) : C --> B /\ `' F : A --> C ) -> ( ( `' G o. g ) o. `' F ) : A --> B )
101	95, 99, 100	syl2anc 643	. . . 4 |- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) : A --> B )
102		mapfien.b	. . . . . 6 |- ( ph -> B e. _V )
103		mapfien.a	. . . . . 6 |- ( ph -> A e. _V )
104		elmapg 6990	. . . . . 6 |- ( ( B e. _V /\ A e. _V ) -> ( ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) <-> ( ( `' G o. g ) o. `' F ) : A --> B ) )
105	102, 103, 104	syl2anc 643	. . . . 5 |- ( ph -> ( ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) <-> ( ( `' G o. g ) o. `' F ) : A --> B ) )
106	105	adantr 452	. . . 4 |- ( ( ph /\ g e. T ) -> ( ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) <-> ( ( `' G o. g ) o. `' F ) : A --> B ) )
107	101, 106	mpbird 224	. . 3 |- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) )
108		f1ofun 5635	. . . . . 6 |- ( F : C -1-1-onto-> A -> Fun F )
109	15, 108	syl 16	. . . . 5 |- ( ph -> Fun F )
110	109	adantr 452	. . . 4 |- ( ( ph /\ g e. T ) -> Fun F )
111		cnvco 5015	. . . . . . 7 |- `' ( `' G o. g ) = ( `' g o. `' `' G )
112	111	imaeq1i 5159	. . . . . 6 |- ( `' ( `' G o. g ) " ( _V \ { Z } ) ) = ( ( `' g o. `' `' G ) " ( _V \ { Z } ) )
113		imaco 5334	. . . . . 6 |- ( ( `' g o. `' `' G ) " ( _V \ { Z } ) ) = ( `' g " ( `' `' G " ( _V \ { Z } ) ) )
114		imacnvcnv 5293	. . . . . . 7 |- ( `' `' G " ( _V \ { Z } ) ) = ( G " ( _V \ { Z } ) )
115	114	imaeq2i 5160	. . . . . 6 |- ( `' g " ( `' `' G " ( _V \ { Z } ) ) ) = ( `' g " ( G " ( _V \ { Z } ) ) )
116	112, 113, 115	3eqtri 2428	. . . . 5 |- ( `' ( `' G o. g ) " ( _V \ { Z } ) ) = ( `' g " ( G " ( _V \ { Z } ) ) )
117	89	a1i 11	. . . . . . 7 |- ( ph -> ( g e. T <-> ( g e. ( D ^m C ) /\ ( `' g " ( _V \ { W } ) ) e. Fin ) ) )
118	117	simplbda 608	. . . . . 6 |- ( ( ph /\ g e. T ) -> ( `' g " ( _V \ { W } ) ) e. Fin )
119	2	adantr 452	. . . . . . . . 9 |- ( ( ph /\ g e. T ) -> G : B -1-1-onto-> D )
120		dff1o3 5639	. . . . . . . . . 10 |- ( G : B -1-1-onto-> D <-> ( G : B -onto-> D /\ Fun `' G ) )
121	120	simprbi 451	. . . . . . . . 9 |- ( G : B -1-1-onto-> D -> Fun `' G )
122		imadif 5487	. . . . . . . . 9 |- ( Fun `' G -> ( G " ( _V \ { Z } ) ) = ( ( G " _V ) \ ( G " { Z } ) ) )
123	119, 121, 122	3syl 19	. . . . . . . 8 |- ( ( ph /\ g e. T ) -> ( G " ( _V \ { Z } ) ) = ( ( G " _V ) \ ( G " { Z } ) ) )
124		ssv 3328	. . . . . . . . . 10 |- ( G " _V ) C_ _V
125		ssdif 3442	. . . . . . . . . 10 |- ( ( G " _V ) C_ _V -> ( ( G " _V ) \ ( G " { Z } ) ) C_ ( _V \ ( G " { Z } ) ) )
126	124, 125	ax-mp 8	. . . . . . . . 9 |- ( ( G " _V ) \ ( G " { Z } ) ) C_ ( _V \ ( G " { Z } ) )
127	119, 3, 60	3syl 19	. . . . . . . . . . . . 13 |- ( ( ph /\ g e. T ) -> G Fn B )
128	52	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ g e. T ) -> Z e. B )
129	128	snssd 3903	. . . . . . . . . . . . 13 |- ( ( ph /\ g e. T ) -> { Z } C_ B )
130		snidg 3799	. . . . . . . . . . . . . 14 |- ( Z e. B -> Z e. { Z } )
131	128, 130	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ g e. T ) -> Z e. { Z } )
132		fnfvima 5935	. . . . . . . . . . . . 13 |- ( ( G Fn B /\ { Z } C_ B /\ Z e. { Z } ) -> ( G ` Z ) e. ( G " { Z } ) )
133	127, 129, 131, 132	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ph /\ g e. T ) -> ( G ` Z ) e. ( G " { Z } ) )
134	54, 133	syl5eqel 2488	. . . . . . . . . . 11 |- ( ( ph /\ g e. T ) -> W e. ( G " { Z } ) )
135	134	snssd 3903	. . . . . . . . . 10 |- ( ( ph /\ g e. T ) -> { W } C_ ( G " { Z } ) )
136	135	sscond 3444	. . . . . . . . 9 |- ( ( ph /\ g e. T ) -> ( _V \ ( G " { Z } ) ) C_ ( _V \ { W } ) )
137	126, 136	syl5ss 3319	. . . . . . . 8 |- ( ( ph /\ g e. T ) -> ( ( G " _V ) \ ( G " { Z } ) ) C_ ( _V \ { W } ) )
138	123, 137	eqsstrd 3342	. . . . . . 7 |- ( ( ph /\ g e. T ) -> ( G " ( _V \ { Z } ) ) C_ ( _V \ { W } ) )
139		imass2 5199	. . . . . . 7 |- ( ( G " ( _V \ { Z } ) ) C_ ( _V \ { W } ) -> ( `' g " ( G " ( _V \ { Z } ) ) ) C_ ( `' g " ( _V \ { W } ) ) )
140	138, 139	syl 16	. . . . . 6 |- ( ( ph /\ g e. T ) -> ( `' g " ( G " ( _V \ { Z } ) ) ) C_ ( `' g " ( _V \ { W } ) ) )
141		ssfi 7288	. . . . . 6 |- ( ( ( `' g " ( _V \ { W } ) ) e. Fin /\ ( `' g " ( G " ( _V \ { Z } ) ) ) C_ ( `' g " ( _V \ { W } ) ) ) -> ( `' g " ( G " ( _V \ { Z } ) ) ) e. Fin )
142	118, 140, 141	syl2anc 643	. . . . 5 |- ( ( ph /\ g e. T ) -> ( `' g " ( G " ( _V \ { Z } ) ) ) e. Fin )
143	116, 142	syl5eqel 2488	. . . 4 |- ( ( ph /\ g e. T ) -> ( `' ( `' G o. g ) " ( _V \ { Z } ) ) e. Fin )
144		imafi 7357	. . . 4 |- ( ( Fun F /\ ( `' ( `' G o. g ) " ( _V \ { Z } ) ) e. Fin ) -> ( F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) ) e. Fin )
145	110, 143, 144	syl2anc 643	. . 3 |- ( ( ph /\ g e. T ) -> ( F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) ) e. Fin )
146		cnveq 5005	. . . . . . . 8 |- ( x = ( ( `' G o. g ) o. `' F ) -> `' x = `' ( ( `' G o. g ) o. `' F ) )
147		cnvco 5015	. . . . . . . 8 |- `' ( ( `' G o. g ) o. `' F ) = ( `' `' F o. `' ( `' G o. g ) )
148	146, 147	syl6eq 2452	. . . . . . 7 |- ( x = ( ( `' G o. g ) o. `' F ) -> `' x = ( `' `' F o. `' ( `' G o. g ) ) )
149	148	imaeq1d 5161	. . . . . 6 |- ( x = ( ( `' G o. g ) o. `' F ) -> ( `' x " ( _V \ { Z } ) ) = ( ( `' `' F o. `' ( `' G o. g ) ) " ( _V \ { Z } ) ) )
150		imaco 5334	. . . . . . 7 |- ( ( `' `' F o. `' ( `' G o. g ) ) " ( _V \ { Z } ) ) = ( `' `' F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) )
151		imacnvcnv 5293	. . . . . . 7 |- ( `' `' F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) ) = ( F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) )
152	150, 151	eqtri 2424	. . . . . 6 |- ( ( `' `' F o. `' ( `' G o. g ) ) " ( _V \ { Z } ) ) = ( F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) )
153	149, 152	syl6eq 2452	. . . . 5 |- ( x = ( ( `' G o. g ) o. `' F ) -> ( `' x " ( _V \ { Z } ) ) = ( F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) ) )
154	153	eleq1d 2470	. . . 4 |- ( x = ( ( `' G o. g ) o. `' F ) -> ( ( `' x " ( _V \ { Z } ) ) e. Fin <-> ( F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) ) e. Fin ) )
155	154, 9	elrab2 3054	. . 3 |- ( ( ( `' G o. g ) o. `' F ) e. S <-> ( ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) /\ ( F " ( `' ( `' G o. g ) " ( _V \ { Z } ) ) ) e. Fin ) )
156	107, 145, 155	sylanbrc 646	. 2 |- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) e. S )
157		coass 5347	. . . . . 6 |- ( ( ( `' G o. g ) o. `' F ) o. F ) = ( ( `' G o. g ) o. ( `' F o. F ) )
158	15	adantr 452	. . . . . . . . 9 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> F : C -1-1-onto-> A )
159		f1ococnv1 5663	. . . . . . . . 9 |- ( F : C -1-1-onto-> A -> ( `' F o. F ) = ( _I |` C ) )
160	158, 159	syl 16	. . . . . . . 8 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' F o. F ) = ( _I |` C ) )
161	160	coeq2d 4994	. . . . . . 7 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( `' F o. F ) ) = ( ( `' G o. g ) o. ( _I |` C ) ) )
162	95	adantrl 697	. . . . . . . 8 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. g ) : C --> B )
163		fcoi1 5576	. . . . . . . 8 |- ( ( `' G o. g ) : C --> B -> ( ( `' G o. g ) o. ( _I |` C ) ) = ( `' G o. g ) )
164	162, 163	syl 16	. . . . . . 7 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( _I |` C ) ) = ( `' G o. g ) )
165	161, 164	eqtrd 2436	. . . . . 6 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( `' F o. F ) ) = ( `' G o. g ) )
166	157, 165	syl5eq 2448	. . . . 5 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( ( `' G o. g ) o. `' F ) o. F ) = ( `' G o. g ) )
167	166	eqeq2d 2415	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> ( f o. F ) = ( `' G o. g ) ) )
168		coass 5347	. . . . . . 7 |- ( ( `' G o. G ) o. ( f o. F ) ) = ( `' G o. ( G o. ( f o. F ) ) )
169	2	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> G : B -1-1-onto-> D )
170		f1ococnv1 5663	. . . . . . . . . 10 |- ( G : B -1-1-onto-> D -> ( `' G o. G ) = ( _I |` B ) )
171	169, 170	syl 16	. . . . . . . . 9 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. G ) = ( _I |` B ) )
172	171	coeq1d 4993	. . . . . . . 8 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. G ) o. ( f o. F ) ) = ( ( _I |` B ) o. ( f o. F ) ) )
173	20	adantrr 698	. . . . . . . . 9 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( f o. F ) : C --> B )
174		fcoi2 5577	. . . . . . . . 9 |- ( ( f o. F ) : C --> B -> ( ( _I |` B ) o. ( f o. F ) ) = ( f o. F ) )
175	173, 174	syl 16	. . . . . . . 8 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( _I |` B ) o. ( f o. F ) ) = ( f o. F ) )
176	172, 175	eqtrd 2436	. . . . . . 7 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. G ) o. ( f o. F ) ) = ( f o. F ) )
177	168, 176	syl5eqr 2450	. . . . . 6 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. ( G o. ( f o. F ) ) ) = ( f o. F ) )
178	177	eqeq2d 2415	. . . . 5 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> ( `' G o. g ) = ( f o. F ) ) )
179		eqcom 2406	. . . . 5 |- ( ( `' G o. g ) = ( f o. F ) <-> ( f o. F ) = ( `' G o. g ) )
180	178, 179	syl6bb 253	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> ( f o. F ) = ( `' G o. g ) ) )
181	167, 180	bitr4d 248	. . 3 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) ) )
182		f1ofo 5640	. . . . 5 |- ( F : C -1-1-onto-> A -> F : C -onto-> A )
183	158, 182	syl 16	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> F : C -onto-> A )
184		ffn 5550	. . . . . 6 |- ( f : A --> B -> f Fn A )
185	12, 13, 184	3syl 19	. . . . 5 |- ( ( ph /\ f e. S ) -> f Fn A )
186	185	adantrr 698	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> f Fn A )
187		ffn 5550	. . . . . 6 |- ( ( ( `' G o. g ) o. `' F ) : A --> B -> ( ( `' G o. g ) o. `' F ) Fn A )
188	101, 187	syl 16	. . . . 5 |- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) Fn A )
189	188	adantrl 697	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. `' F ) Fn A )
190		cocan2 5984	. . . 4 |- ( ( F : C -onto-> A /\ f Fn A /\ ( ( `' G o. g ) o. `' F ) Fn A ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> f = ( ( `' G o. g ) o. `' F ) ) )
191	183, 186, 189, 190	syl3anc 1184	. . 3 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> f = ( ( `' G o. g ) o. `' F ) ) )
192	2, 81	syl 16	. . . . . 6 |- ( ph -> `' G : D -1-1-onto-> B )
193	192	adantr 452	. . . . 5 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> `' G : D -1-1-onto-> B )
194		f1of1 5632	. . . . 5 |- ( `' G : D -1-1-onto-> B -> `' G : D -1-1-> B )
195	193, 194	syl 16	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> `' G : D -1-1-> B )
196	93	adantrl 697	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> g : C --> D )
197	22	adantrr 698	. . . 4 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( G o. ( f o. F ) ) : C --> D )
198		cocan1 5983	. . . 4 |- ( ( `' G : D -1-1-> B /\ g : C --> D /\ ( G o. ( f o. F ) ) : C --> D ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> g = ( G o. ( f o. F ) ) ) )
199	195, 196, 197, 198	syl3anc 1184	. . 3 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> g = ( G o. ( f o. F ) ) ) )
200	181, 191, 199	3bitr3d 275	. 2 |- ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( f = ( ( `' G o. g ) o. `' F ) <-> g = ( G o. ( f o. F ) ) ) )
201	1, 80, 156, 200	f1o2d 6255	1 |- ( ph -> ( f e. S |-> ( G o. ( f o. F ) ) ) : S -1-1-onto-> T )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   {crab 2670   _Vcvv 2916   \ cdif 3277   C_ wss 3280   {csn 3774   e. cmpt 4226   _I cid 4453   `'ccnv 4836   |` cres 4839   "cima 4840   o. ccom 4841   Fun wfun 5407   Fn wfn 5408   -->wf 5409   -1-1->wf1 5410   -onto->wfo 5411   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   ^m cmap 6977   Fincfn 7068

This theorem is referenced by:  wemapwe  7610  oef1o  7611  mapfien2  27126

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-1o 6683  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-fin 7072