Step | Hyp | Ref
| Expression |
1 | | eleq1 2676 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 ∈ Word 𝑉 ↔ 𝑦 ∈ Word 𝑉)) |
2 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
3 | 2 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = 𝑦 → ((#‘𝑥) = ((#‘𝑊) + 1) ↔ (#‘𝑦) = ((#‘𝑊) + 1))) |
4 | 1, 3 | anbi12d 743 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) ↔ (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1)))) |
5 | 4 | cbvralv 3147 |
. 2
⊢
(∀𝑥 ∈
𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) ↔ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) |
6 | | s1eq 13233 |
. . . . . 6
⊢ (𝑣 = 𝑢 → 〈“𝑣”〉 = 〈“𝑢”〉) |
7 | 6 | oveq2d 6565 |
. . . . 5
⊢ (𝑣 = 𝑢 → (𝑊 ++ 〈“𝑣”〉) = (𝑊 ++ 〈“𝑢”〉)) |
8 | 7 | eleq1d 2672 |
. . . 4
⊢ (𝑣 = 𝑢 → ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ↔ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋)) |
9 | 8 | reu8 3369 |
. . 3
⊢
(∃!𝑣 ∈
𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ↔ ∃𝑣 ∈ 𝑉 ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) |
10 | | simprl 790 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋) |
11 | | simp-4l 802 |
. . . . . . . . 9
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → 𝑊 ∈ Word 𝑉) |
12 | | simpr 476 |
. . . . . . . . 9
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
13 | 10 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋) |
14 | | simplrr 797 |
. . . . . . . . 9
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢)) |
15 | | simp-4r 803 |
. . . . . . . . 9
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) |
16 | | reuccats1lem 13331 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋) ∧ (∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢) ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1)))) → (𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉) → 𝑥 = (𝑊 ++ 〈“𝑣”〉))) |
17 | 11, 12, 13, 14, 15, 16 | syl32anc 1326 |
. . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → (𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉) → 𝑥 = (𝑊 ++ 〈“𝑣”〉))) |
18 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑊 ++ 〈“𝑣”〉) → (𝑥 substr 〈0, (#‘𝑊)〉) = ((𝑊 ++ 〈“𝑣”〉) substr 〈0, (#‘𝑊)〉)) |
19 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) → 𝑊 ∈ Word 𝑉) |
20 | | s1cl 13235 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝑉 → 〈“𝑣”〉 ∈ Word 𝑉) |
21 | 19, 20 | anim12i 588 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑣”〉 ∈ Word 𝑉)) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑣”〉 ∈ Word 𝑉)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑣”〉 ∈ Word 𝑉)) |
24 | | swrdccat1 13309 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑣”〉 ∈ Word 𝑉) → ((𝑊 ++ 〈“𝑣”〉) substr 〈0, (#‘𝑊)〉) = 𝑊) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → ((𝑊 ++ 〈“𝑣”〉) substr 〈0, (#‘𝑊)〉) = 𝑊) |
26 | 18, 25 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 = (𝑊 ++ 〈“𝑣”〉)) → (𝑥 substr 〈0, (#‘𝑊)〉) = 𝑊) |
27 | 26 | eqcomd 2616 |
. . . . . . . . 9
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 = (𝑊 ++ 〈“𝑣”〉)) → 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉)) |
28 | 27 | ex 449 |
. . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → (𝑥 = (𝑊 ++ 〈“𝑣”〉) → 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉))) |
29 | 17, 28 | impbid 201 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑥 ∈ 𝑋) → (𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉) ↔ 𝑥 = (𝑊 ++ 〈“𝑣”〉))) |
30 | 29 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → ∀𝑥 ∈ 𝑋 (𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉) ↔ 𝑥 = (𝑊 ++ 〈“𝑣”〉))) |
31 | | reu6i 3364 |
. . . . . 6
⊢ (((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉) ↔ 𝑥 = (𝑊 ++ 〈“𝑣”〉))) → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉)) |
32 | 10, 30, 31 | syl2anc 691 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉)) |
33 | 32 | ex 449 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢)) → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉))) |
34 | 33 | rexlimdva 3013 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) → (∃𝑣 ∈ 𝑉 ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢)) → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉))) |
35 | 9, 34 | syl5bi 231 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑦 ∈ 𝑋 (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = ((#‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉))) |
36 | 5, 35 | sylan2b 491 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉))) |