Step |
Hyp |
Ref |
Expression |
1 |
|
cats2cat.b |
⊢ 𝐵 ∈ Word V |
2 |
|
cats2cat.d |
⊢ 𝐷 ∈ Word V |
3 |
|
cats2cat.a |
⊢ 𝐴 = ( 𝐵 ++ 〈“ 𝑋 ”〉 ) |
4 |
|
cats2cat.c |
⊢ 𝐶 = ( 〈“ 𝑌 ”〉 ++ 𝐷 ) |
5 |
3 4
|
oveq12i |
⊢ ( 𝐴 ++ 𝐶 ) = ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ ( 〈“ 𝑌 ”〉 ++ 𝐷 ) ) |
6 |
|
s1cli |
⊢ 〈“ 𝑋 ”〉 ∈ Word V |
7 |
|
ccatcl |
⊢ ( ( 𝐵 ∈ Word V ∧ 〈“ 𝑋 ”〉 ∈ Word V ) → ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ∈ Word V ) |
8 |
1 6 7
|
mp2an |
⊢ ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ∈ Word V |
9 |
|
s1cli |
⊢ 〈“ 𝑌 ”〉 ∈ Word V |
10 |
|
ccatass |
⊢ ( ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ∈ Word V ∧ 〈“ 𝑌 ”〉 ∈ Word V ∧ 𝐷 ∈ Word V ) → ( ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) ++ 𝐷 ) = ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ ( 〈“ 𝑌 ”〉 ++ 𝐷 ) ) ) |
11 |
8 9 2 10
|
mp3an |
⊢ ( ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) ++ 𝐷 ) = ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ ( 〈“ 𝑌 ”〉 ++ 𝐷 ) ) |
12 |
|
ccatass |
⊢ ( ( 𝐵 ∈ Word V ∧ 〈“ 𝑋 ”〉 ∈ Word V ∧ 〈“ 𝑌 ”〉 ∈ Word V ) → ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) = ( 𝐵 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ) |
13 |
1 6 9 12
|
mp3an |
⊢ ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) = ( 𝐵 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) |
14 |
|
df-s2 |
⊢ 〈“ 𝑋 𝑌 ”〉 = ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) |
15 |
14
|
eqcomi |
⊢ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) = 〈“ 𝑋 𝑌 ”〉 |
16 |
15
|
oveq2i |
⊢ ( 𝐵 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) = ( 𝐵 ++ 〈“ 𝑋 𝑌 ”〉 ) |
17 |
13 16
|
eqtri |
⊢ ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) = ( 𝐵 ++ 〈“ 𝑋 𝑌 ”〉 ) |
18 |
17
|
oveq1i |
⊢ ( ( ( 𝐵 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) ++ 𝐷 ) = ( ( 𝐵 ++ 〈“ 𝑋 𝑌 ”〉 ) ++ 𝐷 ) |
19 |
5 11 18
|
3eqtr2i |
⊢ ( 𝐴 ++ 𝐶 ) = ( ( 𝐵 ++ 〈“ 𝑋 𝑌 ”〉 ) ++ 𝐷 ) |