Step |
Hyp |
Ref |
Expression |
1 |
|
coe1fval.a |
|- A = ( coe1 ` F ) |
2 |
|
coe1f2.b |
|- B = ( Base ` P ) |
3 |
|
coe1f2.p |
|- P = ( PwSer1 ` R ) |
4 |
|
coe1f2.k |
|- K = ( Base ` R ) |
5 |
3 2 4
|
psr1basf |
|- ( F e. B -> F : ( NN0 ^m 1o ) --> K ) |
6 |
|
df1o2 |
|- 1o = { (/) } |
7 |
|
nn0ex |
|- NN0 e. _V |
8 |
|
0ex |
|- (/) e. _V |
9 |
|
eqid |
|- ( x e. NN0 |-> ( 1o X. { x } ) ) = ( x e. NN0 |-> ( 1o X. { x } ) ) |
10 |
6 7 8 9
|
mapsnf1o3 |
|- ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o ) |
11 |
|
f1of |
|- ( ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o ) -> ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 --> ( NN0 ^m 1o ) ) |
12 |
10 11
|
ax-mp |
|- ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 --> ( NN0 ^m 1o ) |
13 |
|
fco |
|- ( ( F : ( NN0 ^m 1o ) --> K /\ ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 --> ( NN0 ^m 1o ) ) -> ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) : NN0 --> K ) |
14 |
5 12 13
|
sylancl |
|- ( F e. B -> ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) : NN0 --> K ) |
15 |
1 2 3 9
|
coe1fval3 |
|- ( F e. B -> A = ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) ) |
16 |
15
|
feq1d |
|- ( F e. B -> ( A : NN0 --> K <-> ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) : NN0 --> K ) ) |
17 |
14 16
|
mpbird |
|- ( F e. B -> A : NN0 --> K ) |