Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
⊢ ( 𝑥 = 𝑈 → ( 𝑥 ∈ Word 𝑉 ↔ 𝑈 ∈ Word 𝑉 ) ) |
2 |
|
fveqeq2 |
⊢ ( 𝑥 = 𝑈 → ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ↔ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) |
3 |
1 2
|
anbi12d |
⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ↔ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ) |
4 |
3
|
rspcv |
⊢ ( 𝑈 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ) |
6 |
|
simpl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) → 𝑊 ∈ Word 𝑉 ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → 𝑊 ∈ Word 𝑉 ) |
8 |
|
simpl |
⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑈 ∈ Word 𝑉 ) |
9 |
8
|
adantl |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → 𝑈 ∈ Word 𝑉 ) |
10 |
|
simprr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) |
11 |
|
ccats1pfxeqrex |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ∃ 𝑢 ∈ 𝑉 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ) ) |
12 |
7 9 10 11
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ∃ 𝑢 ∈ 𝑉 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ) ) |
13 |
|
s1eq |
⊢ ( 𝑠 = 𝑢 → 〈“ 𝑠 ”〉 = 〈“ 𝑢 ”〉 ) |
14 |
13
|
oveq2d |
⊢ ( 𝑠 = 𝑢 → ( 𝑊 ++ 〈“ 𝑠 ”〉 ) = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ) |
15 |
14
|
eleq1d |
⊢ ( 𝑠 = 𝑢 → ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 ↔ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) ) |
16 |
|
eqeq2 |
⊢ ( 𝑠 = 𝑢 → ( 𝑆 = 𝑠 ↔ 𝑆 = 𝑢 ) ) |
17 |
15 16
|
imbi12d |
⊢ ( 𝑠 = 𝑢 → ( ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) ↔ ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ) ) |
18 |
17
|
rspcv |
⊢ ( 𝑢 ∈ 𝑉 → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ) ) |
19 |
|
eleq1 |
⊢ ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → ( 𝑈 ∈ 𝑋 ↔ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) ) |
20 |
|
id |
⊢ ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) → ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ) |
21 |
20
|
imp |
⊢ ( ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ∧ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) → 𝑆 = 𝑢 ) |
22 |
21
|
eqcomd |
⊢ ( ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ∧ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) → 𝑢 = 𝑆 ) |
23 |
22
|
s1eqd |
⊢ ( ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ∧ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) → 〈“ 𝑢 ”〉 = 〈“ 𝑆 ”〉 ) |
24 |
23
|
oveq2d |
⊢ ( ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ∧ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) → ( 𝑊 ++ 〈“ 𝑢 ”〉 ) = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) |
25 |
24
|
eqeq2d |
⊢ ( ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ∧ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) → ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ↔ 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) |
26 |
25
|
biimpd |
⊢ ( ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) ∧ ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 ) → ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) |
27 |
26
|
ex |
⊢ ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) → ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
28 |
27
|
com13 |
⊢ ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
29 |
19 28
|
sylbid |
⊢ ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → ( 𝑈 ∈ 𝑋 → ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
30 |
29
|
com3l |
⊢ ( 𝑈 ∈ 𝑋 → ( ( ( 𝑊 ++ 〈“ 𝑢 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑢 ) → ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
31 |
18 30
|
sylan9r |
⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑢 ∈ 𝑉 ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
32 |
31
|
com23 |
⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑢 ∈ 𝑉 ) → ( 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
33 |
32
|
rexlimdva |
⊢ ( 𝑈 ∈ 𝑋 → ( ∃ 𝑢 ∈ 𝑉 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
34 |
33
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) → ( ∃ 𝑢 ∈ 𝑉 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
35 |
34
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∃ 𝑢 ∈ 𝑉 𝑈 = ( 𝑊 ++ 〈“ 𝑢 ”〉 ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
36 |
12 35
|
syld |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
37 |
36
|
com23 |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) |
38 |
37
|
ex |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) → ( ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) ) |
39 |
5 38
|
syld |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) ) |
40 |
39
|
com23 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) → ( ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) ) ) |
41 |
40
|
3imp |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝑉 ( ( 𝑊 ++ 〈“ 𝑠 ”〉 ) ∈ 𝑋 → 𝑆 = 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) ) |