Step |
Hyp |
Ref |
Expression |
1 |
|
mbfulm.z |
|- Z = ( ZZ>= ` M ) |
2 |
|
mbfulm.m |
|- ( ph -> M e. ZZ ) |
3 |
|
mbfulm.f |
|- ( ph -> F : Z --> MblFn ) |
4 |
|
mbfulm.u |
|- ( ph -> F ( ~~>u ` S ) G ) |
5 |
|
ulmcl |
|- ( F ( ~~>u ` S ) G -> G : S --> CC ) |
6 |
4 5
|
syl |
|- ( ph -> G : S --> CC ) |
7 |
6
|
feqmptd |
|- ( ph -> G = ( z e. S |-> ( G ` z ) ) ) |
8 |
2
|
adantr |
|- ( ( ph /\ z e. S ) -> M e. ZZ ) |
9 |
3
|
ffnd |
|- ( ph -> F Fn Z ) |
10 |
|
ulmf2 |
|- ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> F : Z --> ( CC ^m S ) ) |
11 |
9 4 10
|
syl2anc |
|- ( ph -> F : Z --> ( CC ^m S ) ) |
12 |
11
|
adantr |
|- ( ( ph /\ z e. S ) -> F : Z --> ( CC ^m S ) ) |
13 |
|
simpr |
|- ( ( ph /\ z e. S ) -> z e. S ) |
14 |
1
|
fvexi |
|- Z e. _V |
15 |
14
|
mptex |
|- ( k e. Z |-> ( ( F ` k ) ` z ) ) e. _V |
16 |
15
|
a1i |
|- ( ( ph /\ z e. S ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) e. _V ) |
17 |
|
fveq2 |
|- ( k = n -> ( F ` k ) = ( F ` n ) ) |
18 |
17
|
fveq1d |
|- ( k = n -> ( ( F ` k ) ` z ) = ( ( F ` n ) ` z ) ) |
19 |
|
eqid |
|- ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` z ) ) |
20 |
|
fvex |
|- ( ( F ` n ) ` z ) e. _V |
21 |
18 19 20
|
fvmpt |
|- ( n e. Z -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ` n ) = ( ( F ` n ) ` z ) ) |
22 |
21
|
eqcomd |
|- ( n e. Z -> ( ( F ` n ) ` z ) = ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ` n ) ) |
23 |
22
|
adantl |
|- ( ( ( ph /\ z e. S ) /\ n e. Z ) -> ( ( F ` n ) ` z ) = ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ` n ) ) |
24 |
4
|
adantr |
|- ( ( ph /\ z e. S ) -> F ( ~~>u ` S ) G ) |
25 |
1 8 12 13 16 23 24
|
ulmclm |
|- ( ( ph /\ z e. S ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) ) |
26 |
11
|
ffvelrnda |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) ) |
27 |
|
elmapi |
|- ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC ) |
28 |
26 27
|
syl |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) : S --> CC ) |
29 |
28
|
feqmptd |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( z e. S |-> ( ( F ` k ) ` z ) ) ) |
30 |
3
|
ffvelrnda |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. MblFn ) |
31 |
29 30
|
eqeltrrd |
|- ( ( ph /\ k e. Z ) -> ( z e. S |-> ( ( F ` k ) ` z ) ) e. MblFn ) |
32 |
28
|
ffvelrnda |
|- ( ( ( ph /\ k e. Z ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC ) |
33 |
32
|
anasss |
|- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) e. CC ) |
34 |
1 2 25 31 33
|
mbflim |
|- ( ph -> ( z e. S |-> ( G ` z ) ) e. MblFn ) |
35 |
7 34
|
eqeltrd |
|- ( ph -> G e. MblFn ) |