| Step | Hyp | Ref
| Expression |
| 1 | | s3cl 14918 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑉) |
| 2 | | eqwrd 14595 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑉) → (𝑊 = 〈“𝐴𝐵𝐶”〉 ↔ ((♯‘𝑊) =
(♯‘〈“𝐴𝐵𝐶”〉) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)))) |
| 3 | 1, 2 | sylan2 593 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴𝐵𝐶”〉 ↔ ((♯‘𝑊) =
(♯‘〈“𝐴𝐵𝐶”〉) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)))) |
| 4 | | s3len 14933 |
. . . . 5
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 |
| 5 | 4 | eqeq2i 2750 |
. . . 4
⊢
((♯‘𝑊) =
(♯‘〈“𝐴𝐵𝐶”〉) ↔ (♯‘𝑊) = 3) |
| 6 | 5 | a1i 11 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((♯‘𝑊) = (♯‘〈“𝐴𝐵𝐶”〉) ↔ (♯‘𝑊) = 3)) |
| 7 | 6 | anbi1d 631 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((♯‘𝑊) = (♯‘〈“𝐴𝐵𝐶”〉) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)) ↔ ((♯‘𝑊) = 3 ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖)))) |
| 8 | | oveq2 7439 |
. . . . . 6
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = (0..^3)) |
| 9 | | fzo0to3tp 13791 |
. . . . . 6
⊢ (0..^3) =
{0, 1, 2} |
| 10 | 8, 9 | eqtrdi 2793 |
. . . . 5
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = {0, 1, 2}) |
| 11 | 10 | raleqdv 3326 |
. . . 4
⊢
((♯‘𝑊) =
3 → (∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ ∀𝑖 ∈ {0, 1, 2} (𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖))) |
| 12 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑊‘𝑖) = (𝑊‘0)) |
| 13 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 0 → (〈“𝐴𝐵𝐶”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘0)) |
| 14 | 12, 13 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑖 = 0 → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘0) = (〈“𝐴𝐵𝐶”〉‘0))) |
| 15 | | s3fv0 14930 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
| 16 | 15 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
| 17 | 16 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊‘0) = (〈“𝐴𝐵𝐶”〉‘0) ↔ (𝑊‘0) = 𝐴)) |
| 18 | 14, 17 | sylan9bbr 510 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑖 = 0) → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘0) = 𝐴)) |
| 19 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 1 → (𝑊‘𝑖) = (𝑊‘1)) |
| 20 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 1 → (〈“𝐴𝐵𝐶”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘1)) |
| 21 | 19, 20 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑖 = 1 → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘1) = (〈“𝐴𝐵𝐶”〉‘1))) |
| 22 | | s3fv1 14931 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
| 23 | 22 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
| 24 | 23 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊‘1) = (〈“𝐴𝐵𝐶”〉‘1) ↔ (𝑊‘1) = 𝐵)) |
| 25 | 21, 24 | sylan9bbr 510 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑖 = 1) → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘1) = 𝐵)) |
| 26 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 2 → (𝑊‘𝑖) = (𝑊‘2)) |
| 27 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 2 → (〈“𝐴𝐵𝐶”〉‘𝑖) = (〈“𝐴𝐵𝐶”〉‘2)) |
| 28 | 26, 27 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑖 = 2 → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘2) = (〈“𝐴𝐵𝐶”〉‘2))) |
| 29 | | s3fv2 14932 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
| 30 | 29 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
| 31 | 30 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊‘2) = (〈“𝐴𝐵𝐶”〉‘2) ↔ (𝑊‘2) = 𝐶)) |
| 32 | 28, 31 | sylan9bbr 510 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑖 = 2) → ((𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ (𝑊‘2) = 𝐶)) |
| 33 | | 0zd 12625 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 0 ∈ ℤ) |
| 34 | | 1zzd 12648 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 1 ∈ ℤ) |
| 35 | | 2z 12649 |
. . . . . . 7
⊢ 2 ∈
ℤ |
| 36 | 35 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 2 ∈ ℤ) |
| 37 | 18, 25, 32, 33, 34, 36 | raltpd 4781 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∀𝑖 ∈ {0, 1, 2} (𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶))) |
| 38 | 37 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∀𝑖 ∈ {0, 1, 2} (𝑊‘𝑖) = (〈“𝐴𝐵𝐶”〉‘𝑖) ↔ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶))) |
| 39 | 11, 38 | sylan9bbr 510 |
. . 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) = 𝐶)))) |