Step |
Hyp |
Ref |
Expression |
1 |
|
hasheq0 |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) ) |
2 |
1
|
biimpa |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → 𝑊 = ∅ ) |
3 |
|
s1cli |
⊢ 〈“ ∅ ”〉 ∈ Word V |
4 |
|
ccatlid |
⊢ ( 〈“ ∅ ”〉 ∈ Word V → ( ∅ ++ 〈“ ∅ ”〉 ) = 〈“ ∅ ”〉 ) |
5 |
3 4
|
ax-mp |
⊢ ( ∅ ++ 〈“ ∅ ”〉 ) = 〈“ ∅ ”〉 |
6 |
5
|
fveq1i |
⊢ ( ( ∅ ++ 〈“ ∅ ”〉 ) ‘ 0 ) = ( 〈“ ∅ ”〉 ‘ 0 ) |
7 |
|
0ex |
⊢ ∅ ∈ V |
8 |
|
s1fv |
⊢ ( ∅ ∈ V → ( 〈“ ∅ ”〉 ‘ 0 ) = ∅ ) |
9 |
7 8
|
ax-mp |
⊢ ( 〈“ ∅ ”〉 ‘ 0 ) = ∅ |
10 |
6 9
|
eqtri |
⊢ ( ( ∅ ++ 〈“ ∅ ”〉 ) ‘ 0 ) = ∅ |
11 |
|
id |
⊢ ( 𝑊 = ∅ → 𝑊 = ∅ ) |
12 |
|
fveq1 |
⊢ ( 𝑊 = ∅ → ( 𝑊 ‘ 0 ) = ( ∅ ‘ 0 ) ) |
13 |
|
0fv |
⊢ ( ∅ ‘ 0 ) = ∅ |
14 |
12 13
|
eqtrdi |
⊢ ( 𝑊 = ∅ → ( 𝑊 ‘ 0 ) = ∅ ) |
15 |
14
|
s1eqd |
⊢ ( 𝑊 = ∅ → 〈“ ( 𝑊 ‘ 0 ) ”〉 = 〈“ ∅ ”〉 ) |
16 |
11 15
|
oveq12d |
⊢ ( 𝑊 = ∅ → ( 𝑊 ++ 〈“ ( 𝑊 ‘ 0 ) ”〉 ) = ( ∅ ++ 〈“ ∅ ”〉 ) ) |
17 |
16
|
fveq1d |
⊢ ( 𝑊 = ∅ → ( ( 𝑊 ++ 〈“ ( 𝑊 ‘ 0 ) ”〉 ) ‘ 0 ) = ( ( ∅ ++ 〈“ ∅ ”〉 ) ‘ 0 ) ) |
18 |
10 17 14
|
3eqtr4a |
⊢ ( 𝑊 = ∅ → ( ( 𝑊 ++ 〈“ ( 𝑊 ‘ 0 ) ”〉 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
19 |
2 18
|
syl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( ( 𝑊 ++ 〈“ ( 𝑊 ‘ 0 ) ”〉 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
20 |
1
|
necon3bid |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 ↔ 𝑊 ≠ ∅ ) ) |
21 |
20
|
biimpa |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → 𝑊 ≠ ∅ ) |
22 |
|
lennncl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
23 |
21 22
|
syldan |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
24 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
25 |
23 24
|
sylibr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
26 |
|
ccats1val1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ 〈“ ( 𝑊 ‘ 0 ) ”〉 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
27 |
25 26
|
syldan |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( 𝑊 ++ 〈“ ( 𝑊 ‘ 0 ) ”〉 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
28 |
19 27
|
pm2.61dane |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ 〈“ ( 𝑊 ‘ 0 ) ”〉 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |