Step |
Hyp |
Ref |
Expression |
1 |
|
df-s3 |
⊢ 〈“ 𝐴 𝐵 𝐶 ”〉 = ( 〈“ 𝐴 𝐵 ”〉 ++ 〈“ 𝐶 ”〉 ) |
2 |
1
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 = ( 〈“ 𝐴 𝐵 ”〉 ++ 〈“ 𝐶 ”〉 ) ) |
3 |
|
df-s3 |
⊢ 〈“ 𝐷 𝐸 𝐹 ”〉 = ( 〈“ 𝐷 𝐸 ”〉 ++ 〈“ 𝐹 ”〉 ) |
4 |
3
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → 〈“ 𝐷 𝐸 𝐹 ”〉 = ( 〈“ 𝐷 𝐸 ”〉 ++ 〈“ 𝐹 ”〉 ) ) |
5 |
2 4
|
eqeq12d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → ( 〈“ 𝐴 𝐵 𝐶 ”〉 = 〈“ 𝐷 𝐸 𝐹 ”〉 ↔ ( 〈“ 𝐴 𝐵 ”〉 ++ 〈“ 𝐶 ”〉 ) = ( 〈“ 𝐷 𝐸 ”〉 ++ 〈“ 𝐹 ”〉 ) ) ) |
6 |
|
s2cl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 〈“ 𝐴 𝐵 ”〉 ∈ Word 𝑉 ) |
7 |
|
s1cl |
⊢ ( 𝐶 ∈ 𝑉 → 〈“ 𝐶 ”〉 ∈ Word 𝑉 ) |
8 |
6 7
|
anim12i |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐶 ∈ 𝑉 ) → ( 〈“ 𝐴 𝐵 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐶 ”〉 ∈ Word 𝑉 ) ) |
9 |
8
|
3impa |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 〈“ 𝐴 𝐵 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐶 ”〉 ∈ Word 𝑉 ) ) |
10 |
9
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → ( 〈“ 𝐴 𝐵 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐶 ”〉 ∈ Word 𝑉 ) ) |
11 |
|
s2cl |
⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → 〈“ 𝐷 𝐸 ”〉 ∈ Word 𝑉 ) |
12 |
|
s1cl |
⊢ ( 𝐹 ∈ 𝑉 → 〈“ 𝐹 ”〉 ∈ Word 𝑉 ) |
13 |
11 12
|
anim12i |
⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 ∈ 𝑉 ) → ( 〈“ 𝐷 𝐸 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐹 ”〉 ∈ Word 𝑉 ) ) |
14 |
13
|
3impa |
⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) → ( 〈“ 𝐷 𝐸 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐹 ”〉 ∈ Word 𝑉 ) ) |
15 |
14
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → ( 〈“ 𝐷 𝐸 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐹 ”〉 ∈ Word 𝑉 ) ) |
16 |
|
s2len |
⊢ ( ♯ ‘ 〈“ 𝐴 𝐵 ”〉 ) = 2 |
17 |
|
s2len |
⊢ ( ♯ ‘ 〈“ 𝐷 𝐸 ”〉 ) = 2 |
18 |
16 17
|
eqtr4i |
⊢ ( ♯ ‘ 〈“ 𝐴 𝐵 ”〉 ) = ( ♯ ‘ 〈“ 𝐷 𝐸 ”〉 ) |
19 |
18
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → ( ♯ ‘ 〈“ 𝐴 𝐵 ”〉 ) = ( ♯ ‘ 〈“ 𝐷 𝐸 ”〉 ) ) |
20 |
|
ccatopth |
⊢ ( ( ( 〈“ 𝐴 𝐵 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐶 ”〉 ∈ Word 𝑉 ) ∧ ( 〈“ 𝐷 𝐸 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝐹 ”〉 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 〈“ 𝐴 𝐵 ”〉 ) = ( ♯ ‘ 〈“ 𝐷 𝐸 ”〉 ) ) → ( ( 〈“ 𝐴 𝐵 ”〉 ++ 〈“ 𝐶 ”〉 ) = ( 〈“ 𝐷 𝐸 ”〉 ++ 〈“ 𝐹 ”〉 ) ↔ ( 〈“ 𝐴 𝐵 ”〉 = 〈“ 𝐷 𝐸 ”〉 ∧ 〈“ 𝐶 ”〉 = 〈“ 𝐹 ”〉 ) ) ) |
21 |
10 15 19 20
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → ( ( 〈“ 𝐴 𝐵 ”〉 ++ 〈“ 𝐶 ”〉 ) = ( 〈“ 𝐷 𝐸 ”〉 ++ 〈“ 𝐹 ”〉 ) ↔ ( 〈“ 𝐴 𝐵 ”〉 = 〈“ 𝐷 𝐸 ”〉 ∧ 〈“ 𝐶 ”〉 = 〈“ 𝐹 ”〉 ) ) ) |
22 |
5 21
|
bitrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → ( 〈“ 𝐴 𝐵 𝐶 ”〉 = 〈“ 𝐷 𝐸 𝐹 ”〉 ↔ ( 〈“ 𝐴 𝐵 ”〉 = 〈“ 𝐷 𝐸 ”〉 ∧ 〈“ 𝐶 ”〉 = 〈“ 𝐹 ”〉 ) ) ) |