Step | Hyp | Ref
| Expression |
1 | | s3cl 14588 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑉) |
2 | | eqwrd 14256 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑉) → (𝑊 = 〈“𝐴𝐵𝐶”〉 ↔ ((♯‘𝑊) =
(♯‘〈“𝐴𝐵𝐶”〉) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)))) |
3 | 1, 2 | sylan2 593 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴𝐵𝐶”〉 ↔ ((♯‘𝑊) =
(♯‘〈“𝐴𝐵𝐶”〉) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)))) |
4 | | s3len 14603 |
. . . . 5
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 |
5 | 4 | eqeq2i 2753 |
. . . 4
⊢
((♯‘𝑊) =
(♯‘〈“𝐴𝐵𝐶”〉) ↔ (♯‘𝑊) = 3) |
6 | 5 | a1i 11 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((♯‘𝑊) = (♯‘〈“𝐴𝐵𝐶”〉) ↔ (♯‘𝑊) = 3)) |
7 | 6 | anbi1d 630 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((♯‘𝑊) = (♯‘〈“𝐴𝐵𝐶”〉) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) ↔ ((♯‘𝑊) = 3 ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)))) |
8 | | oveq2 7277 |
. . . . . 6
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = (0..^3)) |
9 | | fzo0to3tp 13469 |
. . . . . 6
⊢ (0..^3) =
{0, 1, 2} |
10 | 8, 9 | eqtrdi 2796 |
. . . . 5
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = {0, 1, 2}) |
11 | 10 | raleqdv 3347 |
. . . 4
⊢
((♯‘𝑊) =
3 → (∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ ∀𝑖 ∈ {0, 1, 2} (𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖))) |
12 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑊‘𝑖) = (𝑊‘0)) |
13 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 0 → (〈“𝐴𝐵𝐶”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘0)) |
14 | 12, 13 | eqeq12d 2756 |
. . . . . . 7
⊢ (𝑖 = 0 → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘0) = (〈“𝐴𝐵𝐶”〉‘0))) |
15 | | s3fv0 14600 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
16 | 15 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
17 | 16 | eqeq2d 2751 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊‘0) = (〈“𝐴𝐵𝐶”〉‘0) ↔ (𝑊‘0) = 𝐴)) |
18 | 14, 17 | sylan9bbr 511 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑖 = 0) → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘0) = 𝐴)) |
19 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 1 → (𝑊‘𝑖) = (𝑊‘1)) |
20 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 1 → (〈“𝐴𝐵𝐶”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘1)) |
21 | 19, 20 | eqeq12d 2756 |
. . . . . . 7
⊢ (𝑖 = 1 → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘1) = (〈“𝐴𝐵𝐶”〉‘1))) |
22 | | s3fv1 14601 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
23 | 22 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
24 | 23 | eqeq2d 2751 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊‘1) = (〈“𝐴𝐵𝐶”〉‘1) ↔ (𝑊‘1) = 𝐵)) |
25 | 21, 24 | sylan9bbr 511 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑖 = 1) → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘1) = 𝐵)) |
26 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 2 → (𝑊‘𝑖) = (𝑊‘2)) |
27 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑖 = 2 → (〈“𝐴𝐵𝐶”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘2)) |
28 | 26, 27 | eqeq12d 2756 |
. . . . . . 7
⊢ (𝑖 = 2 → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘2) = (〈“𝐴𝐵𝐶”〉‘2))) |
29 | | s3fv2 14602 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
30 | 29 | 3ad2ant3 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
31 | 30 | eqeq2d 2751 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊‘2) = (〈“𝐴𝐵𝐶”〉‘2) ↔ (𝑊‘2) = 𝐶)) |
32 | 28, 31 | sylan9bbr 511 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑖 = 2) → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘2) = 𝐶)) |
33 | | 0zd 12329 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 0 ∈ ℤ) |
34 | | 1zzd 12349 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 1 ∈ ℤ) |
35 | | 2z 12350 |
. . . . . . 7
⊢ 2 ∈
ℤ |
36 | 35 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 2 ∈ ℤ) |
37 | 18, 25, 32, 33, 34, 36 | raltpd 4723 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∀𝑖 ∈ {0, 1, 2} (𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶))) |
38 | 37 | adantl 482 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∀𝑖 ∈ {0, 1, 2} (𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶))) |
39 | 11, 38 | sylan9bbr 511 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (♯‘𝑊) = 3) → (∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶))) |
40 | 39 | pm5.32da 579 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((♯‘𝑊) = 3 ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶)))) |
41 | 3, 7, 40 | 3bitrd 305 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴𝐵𝐶”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶)))) |