Step |
Hyp |
Ref |
Expression |
1 |
|
efmnd1bas.1 |
|- G = ( EndoFMnd ` A ) |
2 |
|
efmnd1bas.2 |
|- B = ( Base ` G ) |
3 |
|
efmnd1bas.0 |
|- A = { I } |
4 |
|
snfi |
|- { I } e. Fin |
5 |
3 4
|
eqeltri |
|- A e. Fin |
6 |
1 2
|
efmndhash |
|- ( A e. Fin -> ( # ` B ) = ( ( # ` A ) ^ ( # ` A ) ) ) |
7 |
5 6
|
ax-mp |
|- ( # ` B ) = ( ( # ` A ) ^ ( # ` A ) ) |
8 |
3
|
fveq2i |
|- ( # ` A ) = ( # ` { I } ) |
9 |
|
hashsng |
|- ( I e. V -> ( # ` { I } ) = 1 ) |
10 |
8 9
|
eqtrid |
|- ( I e. V -> ( # ` A ) = 1 ) |
11 |
10 10
|
oveq12d |
|- ( I e. V -> ( ( # ` A ) ^ ( # ` A ) ) = ( 1 ^ 1 ) ) |
12 |
|
1z |
|- 1 e. ZZ |
13 |
|
1exp |
|- ( 1 e. ZZ -> ( 1 ^ 1 ) = 1 ) |
14 |
12 13
|
ax-mp |
|- ( 1 ^ 1 ) = 1 |
15 |
11 14
|
eqtrdi |
|- ( I e. V -> ( ( # ` A ) ^ ( # ` A ) ) = 1 ) |
16 |
7 15
|
eqtrid |
|- ( I e. V -> ( # ` B ) = 1 ) |