Step |
Hyp |
Ref |
Expression |
1 |
|
s1cli |
⊢ 〈“ 𝑋 ”〉 ∈ Word V |
2 |
|
s1cli |
⊢ 〈“ 𝑌 ”〉 ∈ Word V |
3 |
|
ccatlen |
⊢ ( ( 〈“ 𝑋 ”〉 ∈ Word V ∧ 〈“ 𝑌 ”〉 ∈ Word V ) → ( ♯ ‘ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) = ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) ) |
4 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝑋 ”〉 ) = 1 |
5 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝑌 ”〉 ) = 1 |
6 |
4 5
|
oveq12i |
⊢ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) = ( 1 + 1 ) |
7 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
8 |
6 7
|
eqtri |
⊢ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) = 2 |
9 |
3 8
|
eqtrdi |
⊢ ( ( 〈“ 𝑋 ”〉 ∈ Word V ∧ 〈“ 𝑌 ”〉 ∈ Word V ) → ( ♯ ‘ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) = 2 ) |
10 |
1 2 9
|
mp2an |
⊢ ( ♯ ‘ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) = 2 |