Step |
Hyp |
Ref |
Expression |
1 |
|
etransclem30.s |
โข ( ๐ โ ๐ โ { โ , โ } ) |
2 |
|
etransclem30.a |
โข ( ๐ โ ๐ โ ( ( TopOpen โ โfld ) โพt ๐ ) ) |
3 |
|
etransclem30.p |
โข ( ๐ โ ๐ โ โ ) |
4 |
|
etransclem30.m |
โข ( ๐ โ ๐ โ โ0 ) |
5 |
|
etransclem30.f |
โข ๐น = ( ๐ฅ โ ๐ โฆ ( ( ๐ฅ โ ( ๐ โ 1 ) ) ยท โ ๐ โ ( 1 ... ๐ ) ( ( ๐ฅ โ ๐ ) โ ๐ ) ) ) |
6 |
|
etransclem30.n |
โข ( ๐ โ ๐ โ โ0 ) |
7 |
|
etransclem30.h |
โข ๐ป = ( ๐ โ ( 0 ... ๐ ) โฆ ( ๐ฅ โ ๐ โฆ ( ( ๐ฅ โ ๐ ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) |
8 |
|
etransclem30.c |
โข ๐ถ = ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
9 |
|
eqid |
โข ( ๐ฅ โ ๐ โฆ โ ๐ โ ( 0 ... ๐ ) ( ( ๐ป โ ๐ ) โ ๐ฅ ) ) = ( ๐ฅ โ ๐ โฆ โ ๐ โ ( 0 ... ๐ ) ( ( ๐ป โ ๐ ) โ ๐ฅ ) ) |
10 |
1 2 3 4 5 6 7 8 9
|
etransclem29 |
โข ( ๐ โ ( ( ๐ D๐ ๐น ) โ ๐ ) = ( ๐ฅ โ ๐ โฆ ฮฃ ๐ โ ( ๐ถ โ ๐ ) ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) ) ) |