Step |
Hyp |
Ref |
Expression |
1 |
|
mapfien.s |
|- S = { x e. ( B ^m A ) | x finSupp Z } |
2 |
|
mapfien.t |
|- T = { x e. ( D ^m C ) | x finSupp W } |
3 |
|
mapfien.w |
|- W = ( G ` Z ) |
4 |
|
mapfien.f |
|- ( ph -> F : C -1-1-onto-> A ) |
5 |
|
mapfien.g |
|- ( ph -> G : B -1-1-onto-> D ) |
6 |
|
mapfien.a |
|- ( ph -> A e. U ) |
7 |
|
mapfien.b |
|- ( ph -> B e. V ) |
8 |
|
mapfien.c |
|- ( ph -> C e. X ) |
9 |
|
mapfien.d |
|- ( ph -> D e. Y ) |
10 |
|
mapfien.z |
|- ( ph -> Z e. B ) |
11 |
3
|
fvexi |
|- W e. _V |
12 |
11
|
a1i |
|- ( ( ph /\ f e. S ) -> W e. _V ) |
13 |
10
|
adantr |
|- ( ( ph /\ f e. S ) -> Z e. B ) |
14 |
|
elrabi |
|- ( f e. { x e. ( B ^m A ) | x finSupp Z } -> f e. ( B ^m A ) ) |
15 |
|
elmapi |
|- ( f e. ( B ^m A ) -> f : A --> B ) |
16 |
14 15
|
syl |
|- ( f e. { x e. ( B ^m A ) | x finSupp Z } -> f : A --> B ) |
17 |
16 1
|
eleq2s |
|- ( f e. S -> f : A --> B ) |
18 |
|
f1of |
|- ( F : C -1-1-onto-> A -> F : C --> A ) |
19 |
4 18
|
syl |
|- ( ph -> F : C --> A ) |
20 |
|
fco |
|- ( ( f : A --> B /\ F : C --> A ) -> ( f o. F ) : C --> B ) |
21 |
17 19 20
|
syl2anr |
|- ( ( ph /\ f e. S ) -> ( f o. F ) : C --> B ) |
22 |
|
f1of |
|- ( G : B -1-1-onto-> D -> G : B --> D ) |
23 |
5 22
|
syl |
|- ( ph -> G : B --> D ) |
24 |
23
|
adantr |
|- ( ( ph /\ f e. S ) -> G : B --> D ) |
25 |
|
ssidd |
|- ( ( ph /\ f e. S ) -> B C_ B ) |
26 |
8
|
adantr |
|- ( ( ph /\ f e. S ) -> C e. X ) |
27 |
7
|
adantr |
|- ( ( ph /\ f e. S ) -> B e. V ) |
28 |
|
breq1 |
|- ( x = f -> ( x finSupp Z <-> f finSupp Z ) ) |
29 |
28 1
|
elrab2 |
|- ( f e. S <-> ( f e. ( B ^m A ) /\ f finSupp Z ) ) |
30 |
29
|
simprbi |
|- ( f e. S -> f finSupp Z ) |
31 |
30
|
adantl |
|- ( ( ph /\ f e. S ) -> f finSupp Z ) |
32 |
|
f1of1 |
|- ( F : C -1-1-onto-> A -> F : C -1-1-> A ) |
33 |
4 32
|
syl |
|- ( ph -> F : C -1-1-> A ) |
34 |
33
|
adantr |
|- ( ( ph /\ f e. S ) -> F : C -1-1-> A ) |
35 |
|
simpr |
|- ( ( ph /\ f e. S ) -> f e. S ) |
36 |
31 34 13 35
|
fsuppco |
|- ( ( ph /\ f e. S ) -> ( f o. F ) finSupp Z ) |
37 |
3
|
eqcomi |
|- ( G ` Z ) = W |
38 |
37
|
a1i |
|- ( ( ph /\ f e. S ) -> ( G ` Z ) = W ) |
39 |
12 13 21 24 25 26 27 36 38
|
fsuppcor |
|- ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) finSupp W ) |