Step |
Hyp |
Ref |
Expression |
1 |
|
cats1cld.1 |
⊢ 𝑇 = ( 𝑆 ++ 〈“ 𝑋 ”〉 ) |
2 |
|
cats1cli.2 |
⊢ 𝑆 ∈ Word V |
3 |
|
cats1fvn.3 |
⊢ ( ♯ ‘ 𝑆 ) = 𝑀 |
4 |
3
|
oveq2i |
⊢ ( 0 + ( ♯ ‘ 𝑆 ) ) = ( 0 + 𝑀 ) |
5 |
|
lencl |
⊢ ( 𝑆 ∈ Word V → ( ♯ ‘ 𝑆 ) ∈ ℕ0 ) |
6 |
2 5
|
ax-mp |
⊢ ( ♯ ‘ 𝑆 ) ∈ ℕ0 |
7 |
3 6
|
eqeltrri |
⊢ 𝑀 ∈ ℕ0 |
8 |
7
|
nn0cni |
⊢ 𝑀 ∈ ℂ |
9 |
8
|
addid2i |
⊢ ( 0 + 𝑀 ) = 𝑀 |
10 |
4 9
|
eqtr2i |
⊢ 𝑀 = ( 0 + ( ♯ ‘ 𝑆 ) ) |
11 |
1 10
|
fveq12i |
⊢ ( 𝑇 ‘ 𝑀 ) = ( ( 𝑆 ++ 〈“ 𝑋 ”〉 ) ‘ ( 0 + ( ♯ ‘ 𝑆 ) ) ) |
12 |
|
s1cli |
⊢ 〈“ 𝑋 ”〉 ∈ Word V |
13 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝑋 ”〉 ) = 1 |
14 |
|
1nn |
⊢ 1 ∈ ℕ |
15 |
13 14
|
eqeltri |
⊢ ( ♯ ‘ 〈“ 𝑋 ”〉 ) ∈ ℕ |
16 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) ↔ ( ♯ ‘ 〈“ 𝑋 ”〉 ) ∈ ℕ ) |
17 |
15 16
|
mpbir |
⊢ 0 ∈ ( 0 ..^ ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) |
18 |
|
ccatval3 |
⊢ ( ( 𝑆 ∈ Word V ∧ 〈“ 𝑋 ”〉 ∈ Word V ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) ) → ( ( 𝑆 ++ 〈“ 𝑋 ”〉 ) ‘ ( 0 + ( ♯ ‘ 𝑆 ) ) ) = ( 〈“ 𝑋 ”〉 ‘ 0 ) ) |
19 |
2 12 17 18
|
mp3an |
⊢ ( ( 𝑆 ++ 〈“ 𝑋 ”〉 ) ‘ ( 0 + ( ♯ ‘ 𝑆 ) ) ) = ( 〈“ 𝑋 ”〉 ‘ 0 ) |
20 |
11 19
|
eqtri |
⊢ ( 𝑇 ‘ 𝑀 ) = ( 〈“ 𝑋 ”〉 ‘ 0 ) |
21 |
|
s1fv |
⊢ ( 𝑋 ∈ 𝑉 → ( 〈“ 𝑋 ”〉 ‘ 0 ) = 𝑋 ) |
22 |
20 21
|
eqtrid |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝑇 ‘ 𝑀 ) = 𝑋 ) |