Step | Hyp | Ref
| Expression |
1 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝑈 → (𝑥 ∈ Word 𝑉 ↔ 𝑈 ∈ Word 𝑉)) |
2 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑈 → (#‘𝑥) = (#‘𝑈)) |
3 | 2 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑥 = 𝑈 → ((#‘𝑥) = ((#‘𝑊) + 1) ↔ (#‘𝑈) = ((#‘𝑊) + 1))) |
4 | 1, 3 | anbi12d 743 |
. . . . . 6
⊢ (𝑥 = 𝑈 → ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) ↔ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)))) |
5 | 4 | rspcv 3278 |
. . . . 5
⊢ (𝑈 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) → (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)))) |
6 | 5 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) → (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)))) |
7 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) → 𝑊 ∈ Word 𝑉) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1))) → 𝑊 ∈ Word 𝑉) |
9 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → 𝑈 ∈ Word 𝑉) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1))) → 𝑈 ∈ Word 𝑉) |
11 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1))) → (#‘𝑈) = ((#‘𝑊) + 1)) |
12 | | ccats1pfxeqrex 40285 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) → ∃𝑢 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑢”〉))) |
13 | 8, 10, 11, 12 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1))) → (𝑊 = (𝑈 prefix (#‘𝑊)) → ∃𝑢 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑢”〉))) |
14 | | s1eq 13233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑢 → 〈“𝑠”〉 = 〈“𝑢”〉) |
15 | 14 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑢 → (𝑊 ++ 〈“𝑠”〉) = (𝑊 ++ 〈“𝑢”〉)) |
16 | 15 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑢 → ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 ↔ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋)) |
17 | | eqeq2 2621 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑢 → (𝑆 = 𝑠 ↔ 𝑆 = 𝑢)) |
18 | 16, 17 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑢 → (((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) ↔ ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢))) |
19 | 18 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝑉 → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢))) |
20 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑈 = (𝑊 ++ 〈“𝑢”〉) → (𝑈 ∈ 𝑋 ↔ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋)) |
21 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) → ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢)) |
22 | 21 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) ∧ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋) → 𝑆 = 𝑢) |
23 | 22 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) ∧ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋) → 𝑢 = 𝑆) |
24 | 23 | s1eqd 13234 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) ∧ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋) → 〈“𝑢”〉 = 〈“𝑆”〉) |
25 | 24 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) ∧ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋) → (𝑊 ++ 〈“𝑢”〉) = (𝑊 ++ 〈“𝑆”〉)) |
26 | 25 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) ∧ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋) → (𝑈 = (𝑊 ++ 〈“𝑢”〉) ↔ 𝑈 = (𝑊 ++ 〈“𝑆”〉))) |
27 | 26 | biimpd 218 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) ∧ (𝑊 ++ 〈“𝑢”〉) ∈ 𝑋) → (𝑈 = (𝑊 ++ 〈“𝑢”〉) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))) |
28 | 27 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) → ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → (𝑈 = (𝑊 ++ 〈“𝑢”〉) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
29 | 28 | com13 86 |
. . . . . . . . . . . . . 14
⊢ (𝑈 = (𝑊 ++ 〈“𝑢”〉) → ((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → (((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
30 | 20, 29 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ (𝑈 = (𝑊 ++ 〈“𝑢”〉) → (𝑈 ∈ 𝑋 → (((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
31 | 30 | com3l 87 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝑋 → (((𝑊 ++ 〈“𝑢”〉) ∈ 𝑋 → 𝑆 = 𝑢) → (𝑈 = (𝑊 ++ 〈“𝑢”〉) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
32 | 19, 31 | sylan9r 688 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑋 ∧ 𝑢 ∈ 𝑉) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → (𝑈 = (𝑊 ++ 〈“𝑢”〉) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
33 | 32 | com23 84 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ 𝑋 ∧ 𝑢 ∈ 𝑉) → (𝑈 = (𝑊 ++ 〈“𝑢”〉) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
34 | 33 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝑋 → (∃𝑢 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑢”〉) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
35 | 34 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) → (∃𝑢 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑢”〉) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1))) → (∃𝑢 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑢”〉) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
37 | 13, 36 | syld 46 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1))) → (𝑊 = (𝑈 prefix (#‘𝑊)) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
38 | 37 | com23 84 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ (𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1))) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“𝑆”〉)))) |
39 | 38 | ex 449 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) → ((𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))))) |
40 | 6, 39 | syld 46 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))))) |
41 | 40 | com23 84 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) → (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) → (∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))))) |
42 | 41 | 3imp 1249 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ ∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))) |