Step | Hyp | Ref
| Expression |
1 | | s1eq 13233 |
. . . . 5
⊢ (𝑣 = 𝑢 → 〈“𝑣”〉 = 〈“𝑢”〉) |
2 | 1 | oveq2d 6565 |
. . . 4
⊢ (𝑣 = 𝑢 → (𝑊 ++ 〈“𝑣”〉) = (𝑊 ++ 〈“𝑢”〉)) |
3 | 2 | eleq1d 2672 |
. . 3
⊢ (𝑣 = 𝑢 → ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ↔ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋)) |
4 | 3 | reu8 3369 |
. 2
⊢
(∃!𝑣 ∈
𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ↔ ∃𝑣 ∈ 𝑉 ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) |
5 | | simprl 790 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋) |
6 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → 𝑊 ∈ Word 𝑉) |
7 | 6 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → 𝑊 ∈ Word 𝑉) |
8 | 7 | anim1i 590 |
. . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ 𝑋)) |
9 | | simplrr 797 |
. . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) → ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢)) |
10 | | simp-4r 803 |
. . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) |
11 | | reuccatpfxs1lem 40296 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ 𝑋) ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (𝑊 = (𝑤 prefix (#‘𝑊)) → 𝑤 = (𝑊 ++ 〈“𝑣”〉))) |
12 | 8, 9, 10, 11 | syl3anc 1318 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (𝑊 = (𝑤 prefix (#‘𝑊)) → 𝑤 = (𝑊 ++ 〈“𝑣”〉))) |
13 | 6 | anim1i 590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉)) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → (𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉)) |
15 | 14 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → (𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉)) |
16 | | lswccats1 13263 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉) → ( lastS ‘(𝑊 ++ 〈“𝑣”〉)) = 𝑣) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → ( lastS ‘(𝑊 ++ 〈“𝑣”〉)) = 𝑣) |
18 | 17 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → 𝑣 = ( lastS ‘(𝑊 ++ 〈“𝑣”〉))) |
19 | 18 | s1eqd 13234 |
. . . . . . . . . . 11
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → 〈“𝑣”〉 = 〈“(
lastS ‘(𝑊 ++
〈“𝑣”〉))”〉) |
20 | 19 | oveq2d 6565 |
. . . . . . . . . 10
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → (𝑊 ++ 〈“𝑣”〉) = (𝑊 ++ 〈“( lastS ‘(𝑊 ++ 〈“𝑣”〉))”〉)) |
21 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → 𝑤 = (𝑊 ++ 〈“𝑣”〉)) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → ( lastS ‘𝑤) = ( lastS ‘(𝑊 ++ 〈“𝑣”〉))) |
23 | 22 | s1eqd 13234 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → 〈“( lastS
‘𝑤)”〉 =
〈“( lastS ‘(𝑊 ++ 〈“𝑣”〉))”〉) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (𝑊 ++ 〈“( lastS ‘𝑤)”〉) = (𝑊 ++ 〈“( lastS
‘(𝑊 ++
〈“𝑣”〉))”〉)) |
25 | 21, 24 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (𝑤 = (𝑊 ++ 〈“( lastS ‘𝑤)”〉) ↔ (𝑊 ++ 〈“𝑣”〉) = (𝑊 ++ 〈“( lastS
‘(𝑊 ++
〈“𝑣”〉))”〉))) |
26 | 25 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → (𝑤 = (𝑊 ++ 〈“( lastS ‘𝑤)”〉) ↔ (𝑊 ++ 〈“𝑣”〉) = (𝑊 ++ 〈“( lastS
‘(𝑊 ++
〈“𝑣”〉))”〉))) |
27 | 20, 26 | mpbird 246 |
. . . . . . . . 9
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → 𝑤 = (𝑊 ++ 〈“( lastS ‘𝑤)”〉)) |
28 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (𝑥 ∈ Word 𝑉 ↔ 𝑤 ∈ Word 𝑉)) |
29 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (#‘𝑥) = (#‘𝑤)) |
30 | 29 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → ((#‘𝑥) = ((#‘𝑊) + 1) ↔ (#‘𝑤) = ((#‘𝑊) + 1))) |
31 | 28, 30 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) ↔ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)))) |
32 | 31 | rspcva 3280 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1))) |
33 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)) ↔ (𝑊 ∈ Word 𝑉 ∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)))) |
34 | 33 | simplbi2com 655 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)) → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)))) |
35 | 32, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)))) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1))))) |
37 | 36 | com13 86 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → (∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) → (𝑤 ∈ 𝑋 → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1))))) |
38 | 37 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (𝑤 ∈ 𝑋 → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)))) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → (𝑤 ∈ 𝑋 → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)))) |
40 | 39 | imp 444 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1))) |
41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → (𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1))) |
42 | | ccats1pfxeqbi 40294 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((#‘𝑊) + 1)) → (𝑊 = (𝑤 prefix (#‘𝑊)) ↔ 𝑤 = (𝑊 ++ 〈“( lastS ‘𝑤)”〉))) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → (𝑊 = (𝑤 prefix (#‘𝑊)) ↔ 𝑤 = (𝑊 ++ 〈“( lastS ‘𝑤)”〉))) |
44 | 27, 43 | mpbird 246 |
. . . . . . . 8
⊢
((((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ 𝑤 = (𝑊 ++ 〈“𝑣”〉)) → 𝑊 = (𝑤 prefix (#‘𝑊))) |
45 | 44 | ex 449 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (𝑤 = (𝑊 ++ 〈“𝑣”〉) → 𝑊 = (𝑤 prefix (#‘𝑊)))) |
46 | 12, 45 | impbid 201 |
. . . . . 6
⊢
(((((𝑊 ∈ Word
𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (𝑊 = (𝑤 prefix (#‘𝑊)) ↔ 𝑤 = (𝑊 ++ 〈“𝑣”〉))) |
47 | 46 | ralrimiva 2949 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → ∀𝑤 ∈ 𝑋 (𝑊 = (𝑤 prefix (#‘𝑊)) ↔ 𝑤 = (𝑊 ++ 〈“𝑣”〉))) |
48 | | reu6i 3364 |
. . . . 5
⊢ (((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 (𝑊 = (𝑤 prefix (#‘𝑊)) ↔ 𝑤 = (𝑊 ++ 〈“𝑣”〉))) → ∃!𝑤 ∈ 𝑋 𝑊 = (𝑤 prefix (#‘𝑊))) |
49 | 5, 47, 48 | syl2anc 691 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) ∧ ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢))) → ∃!𝑤 ∈ 𝑋 𝑊 = (𝑤 prefix (#‘𝑊))) |
50 | 49 | ex 449 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢)) → ∃!𝑤 ∈ 𝑋 𝑊 = (𝑤 prefix (#‘𝑊)))) |
51 | 50 | rexlimdva 3013 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (∃𝑣 ∈ 𝑉 ((𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑉 ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑣 = 𝑢)) → ∃!𝑤 ∈ 𝑋 𝑊 = (𝑤 prefix (#‘𝑊)))) |
52 | 4, 51 | syl5bi 231 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 → ∃!𝑤 ∈ 𝑋 𝑊 = (𝑤 prefix (#‘𝑊)))) |