Step |
Hyp |
Ref |
Expression |
1 |
|
wrd0 |
|- (/) e. Word _V |
2 |
|
revlen |
|- ( (/) e. Word _V -> ( # ` ( reverse ` (/) ) ) = ( # ` (/) ) ) |
3 |
1 2
|
ax-mp |
|- ( # ` ( reverse ` (/) ) ) = ( # ` (/) ) |
4 |
|
hash0 |
|- ( # ` (/) ) = 0 |
5 |
3 4
|
eqtri |
|- ( # ` ( reverse ` (/) ) ) = 0 |
6 |
|
fvex |
|- ( reverse ` (/) ) e. _V |
7 |
|
hasheq0 |
|- ( ( reverse ` (/) ) e. _V -> ( ( # ` ( reverse ` (/) ) ) = 0 <-> ( reverse ` (/) ) = (/) ) ) |
8 |
6 7
|
ax-mp |
|- ( ( # ` ( reverse ` (/) ) ) = 0 <-> ( reverse ` (/) ) = (/) ) |
9 |
5 8
|
mpbi |
|- ( reverse ` (/) ) = (/) |