Step |
Hyp |
Ref |
Expression |
1 |
|
wrd2ind.1 |
⊢ ( ( 𝑥 = ∅ ∧ 𝑤 = ∅ ) → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
wrd2ind.2 |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑤 = 𝑢 ) → ( 𝜑 ↔ 𝜒 ) ) |
3 |
|
wrd2ind.3 |
⊢ ( ( 𝑥 = ( 𝑦 ++ 〈“ 𝑧 ”〉 ) ∧ 𝑤 = ( 𝑢 ++ 〈“ 𝑠 ”〉 ) ) → ( 𝜑 ↔ 𝜃 ) ) |
4 |
|
wrd2ind.4 |
⊢ ( 𝑥 = 𝐴 → ( 𝜌 ↔ 𝜏 ) ) |
5 |
|
wrd2ind.5 |
⊢ ( 𝑤 = 𝐵 → ( 𝜑 ↔ 𝜌 ) ) |
6 |
|
wrd2ind.6 |
⊢ 𝜓 |
7 |
|
wrd2ind.7 |
⊢ ( ( ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝜒 → 𝜃 ) ) |
8 |
|
lencl |
⊢ ( 𝐴 ∈ Word 𝑋 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) |
9 |
|
eqeq2 |
⊢ ( 𝑛 = 0 → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = 0 ) ) |
10 |
9
|
anbi2d |
⊢ ( 𝑛 = 0 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) ) ) |
11 |
10
|
imbi1d |
⊢ ( 𝑛 = 0 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 ) ) ) |
12 |
11
|
2ralbidv |
⊢ ( 𝑛 = 0 → ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 ) ) ) |
13 |
|
eqeq2 |
⊢ ( 𝑛 = 𝑚 → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = 𝑚 ) ) |
14 |
13
|
anbi2d |
⊢ ( 𝑛 = 𝑚 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) ) ) |
15 |
14
|
imbi1d |
⊢ ( 𝑛 = 𝑚 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ) ) |
16 |
15
|
2ralbidv |
⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ) ) |
17 |
|
eqeq2 |
⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) |
18 |
17
|
anbi2d |
⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) |
19 |
18
|
imbi1d |
⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) ) |
20 |
19
|
2ralbidv |
⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) ) |
21 |
|
eqeq2 |
⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ) |
22 |
21
|
anbi2d |
⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ) ) |
23 |
22
|
imbi1d |
⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ) ) |
24 |
23
|
2ralbidv |
⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ) ) |
25 |
|
eqeq1 |
⊢ ( ( ♯ ‘ 𝑥 ) = 0 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ 0 = ( ♯ ‘ 𝑤 ) ) ) |
26 |
25
|
adantl |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ 0 = ( ♯ ‘ 𝑤 ) ) ) |
27 |
|
eqcom |
⊢ ( 0 = ( ♯ ‘ 𝑤 ) ↔ ( ♯ ‘ 𝑤 ) = 0 ) |
28 |
|
hasheq0 |
⊢ ( 𝑤 ∈ Word 𝑌 → ( ( ♯ ‘ 𝑤 ) = 0 ↔ 𝑤 = ∅ ) ) |
29 |
27 28
|
syl5bb |
⊢ ( 𝑤 ∈ Word 𝑌 → ( 0 = ( ♯ ‘ 𝑤 ) ↔ 𝑤 = ∅ ) ) |
30 |
|
hasheq0 |
⊢ ( 𝑥 ∈ Word 𝑋 → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) ) |
31 |
6 1
|
mpbiri |
⊢ ( ( 𝑥 = ∅ ∧ 𝑤 = ∅ ) → 𝜑 ) |
32 |
31
|
ex |
⊢ ( 𝑥 = ∅ → ( 𝑤 = ∅ → 𝜑 ) ) |
33 |
30 32
|
syl6bi |
⊢ ( 𝑥 ∈ Word 𝑋 → ( ( ♯ ‘ 𝑥 ) = 0 → ( 𝑤 = ∅ → 𝜑 ) ) ) |
34 |
33
|
com13 |
⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑥 ) = 0 → ( 𝑥 ∈ Word 𝑋 → 𝜑 ) ) ) |
35 |
29 34
|
syl6bi |
⊢ ( 𝑤 ∈ Word 𝑌 → ( 0 = ( ♯ ‘ 𝑤 ) → ( ( ♯ ‘ 𝑥 ) = 0 → ( 𝑥 ∈ Word 𝑋 → 𝜑 ) ) ) ) |
36 |
35
|
com24 |
⊢ ( 𝑤 ∈ Word 𝑌 → ( 𝑥 ∈ Word 𝑋 → ( ( ♯ ‘ 𝑥 ) = 0 → ( 0 = ( ♯ ‘ 𝑤 ) → 𝜑 ) ) ) ) |
37 |
36
|
imp31 |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → ( 0 = ( ♯ ‘ 𝑤 ) → 𝜑 ) ) |
38 |
26 37
|
sylbid |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → 𝜑 ) ) |
39 |
38
|
ex |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) → ( ( ♯ ‘ 𝑥 ) = 0 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → 𝜑 ) ) ) |
40 |
39
|
impcomd |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 ) ) |
41 |
40
|
rgen2 |
⊢ ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 ) |
42 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) |
43 |
|
fveq2 |
⊢ ( 𝑤 = 𝑢 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ) |
44 |
42 43
|
eqeqan12d |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑤 = 𝑢 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) ) |
45 |
|
fveqeq2 |
⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) = 𝑚 ↔ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) |
46 |
45
|
adantr |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑤 = 𝑢 ) → ( ( ♯ ‘ 𝑥 ) = 𝑚 ↔ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) |
47 |
44 46
|
anbi12d |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑤 = 𝑢 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) ↔ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) ) |
48 |
47 2
|
imbi12d |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑤 = 𝑢 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ) |
49 |
48
|
ancoms |
⊢ ( ( 𝑤 = 𝑢 ∧ 𝑥 = 𝑦 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ) |
50 |
49
|
cbvraldva |
⊢ ( 𝑤 = 𝑢 → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ) |
51 |
50
|
cbvralvw |
⊢ ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) |
52 |
|
pfxcl |
⊢ ( 𝑤 ∈ Word 𝑌 → ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ) |
53 |
52
|
adantr |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) → ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ) |
54 |
53
|
ad2antrl |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ) |
55 |
|
simprll |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ∈ Word 𝑌 ) |
56 |
|
eqeq1 |
⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ ( 𝑚 + 1 ) = ( ♯ ‘ 𝑤 ) ) ) |
57 |
|
nn0p1nn |
⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ ) |
58 |
|
eleq1 |
⊢ ( ( ♯ ‘ 𝑤 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ ( 𝑚 + 1 ) ∈ ℕ ) ) |
59 |
58
|
eqcoms |
⊢ ( ( 𝑚 + 1 ) = ( ♯ ‘ 𝑤 ) → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ ( 𝑚 + 1 ) ∈ ℕ ) ) |
60 |
57 59
|
syl5ibr |
⊢ ( ( 𝑚 + 1 ) = ( ♯ ‘ 𝑤 ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) ) |
61 |
56 60
|
syl6bi |
⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) ) ) |
62 |
61
|
impcom |
⊢ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) ) |
63 |
62
|
adantl |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) ) |
64 |
63
|
impcom |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ ) |
65 |
64
|
nnge1d |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 1 ≤ ( ♯ ‘ 𝑤 ) ) |
66 |
|
wrdlenge1n0 |
⊢ ( 𝑤 ∈ Word 𝑌 → ( 𝑤 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) |
67 |
55 66
|
syl |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑤 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑤 ) ) ) |
68 |
65 67
|
mpbird |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ≠ ∅ ) |
69 |
|
lswcl |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅ ) → ( lastS ‘ 𝑤 ) ∈ 𝑌 ) |
70 |
55 68 69
|
syl2anc |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( lastS ‘ 𝑤 ) ∈ 𝑌 ) |
71 |
54 70
|
jca |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) ) |
72 |
|
pfxcl |
⊢ ( 𝑥 ∈ Word 𝑋 → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ) |
73 |
72
|
adantl |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ) |
74 |
73
|
ad2antrl |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ) |
75 |
|
simprlr |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ∈ Word 𝑋 ) |
76 |
|
eleq1 |
⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ ( 𝑚 + 1 ) ∈ ℕ ) ) |
77 |
57 76
|
syl5ibr |
⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑥 ) ∈ ℕ ) ) |
78 |
77
|
ad2antll |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑥 ) ∈ ℕ ) ) |
79 |
78
|
impcom |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ ) |
80 |
79
|
nnge1d |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 1 ≤ ( ♯ ‘ 𝑥 ) ) |
81 |
|
wrdlenge1n0 |
⊢ ( 𝑥 ∈ Word 𝑋 → ( 𝑥 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑥 ) ) ) |
82 |
75 81
|
syl |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑥 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑥 ) ) ) |
83 |
80 82
|
mpbird |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ≠ ∅ ) |
84 |
|
lswcl |
⊢ ( ( 𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅ ) → ( lastS ‘ 𝑥 ) ∈ 𝑋 ) |
85 |
75 83 84
|
syl2anc |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( lastS ‘ 𝑥 ) ∈ 𝑋 ) |
86 |
71 74 85
|
jca32 |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ∧ ( lastS ‘ 𝑥 ) ∈ 𝑋 ) ) ) |
87 |
86
|
adantlr |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ∧ ( lastS ‘ 𝑥 ) ∈ 𝑋 ) ) ) |
88 |
|
simprl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ) |
89 |
|
simplr |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) |
90 |
|
simprrl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ) |
91 |
90
|
oveq1d |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) = ( ( ♯ ‘ 𝑤 ) − 1 ) ) |
92 |
|
simprlr |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ∈ Word 𝑋 ) |
93 |
|
fzossfz |
⊢ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑥 ) ) |
94 |
|
simprrr |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) |
95 |
57
|
ad2antrr |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑚 + 1 ) ∈ ℕ ) |
96 |
94 95
|
eqeltrd |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ ) |
97 |
|
fzo0end |
⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℕ → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ) |
98 |
96 97
|
syl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ) |
99 |
93 98
|
sselid |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) |
100 |
|
pfxlen |
⊢ ( ( 𝑥 ∈ Word 𝑋 ∧ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑥 ) − 1 ) ) |
101 |
92 99 100
|
syl2anc |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑥 ) − 1 ) ) |
102 |
|
simprll |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ∈ Word 𝑌 ) |
103 |
|
oveq1 |
⊢ ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( ( ♯ ‘ 𝑥 ) − 1 ) ) |
104 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) → ( 0 ... ( ♯ ‘ 𝑤 ) ) = ( 0 ... ( ♯ ‘ 𝑥 ) ) ) |
105 |
103 104
|
eleq12d |
⊢ ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) |
106 |
105
|
eqcoms |
⊢ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) |
107 |
106
|
adantr |
⊢ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) |
108 |
107
|
ad2antll |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) |
109 |
99 108
|
mpbird |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) |
110 |
|
pfxlen |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑤 ) − 1 ) ) |
111 |
102 109 110
|
syl2anc |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑤 ) − 1 ) ) |
112 |
91 101 111
|
3eqtr4d |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) |
113 |
94
|
oveq1d |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) = ( ( 𝑚 + 1 ) − 1 ) ) |
114 |
|
nn0cn |
⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ ) |
115 |
114
|
ad2antrr |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑚 ∈ ℂ ) |
116 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
117 |
|
pncan |
⊢ ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 ) |
118 |
115 116 117
|
sylancl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 ) |
119 |
101 113 118
|
3eqtrd |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) |
120 |
112 119
|
jca |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) ) |
121 |
73
|
adantr |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ) |
122 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) ) |
123 |
|
fveq2 |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) |
124 |
122 123
|
eqeqan12d |
⊢ ( ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) |
125 |
124
|
expcom |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) ) |
126 |
125
|
adantl |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) ) |
127 |
126
|
imp |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) |
128 |
|
fveqeq2 |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = 𝑚 ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) ) |
129 |
128
|
adantl |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑦 ) = 𝑚 ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) ) |
130 |
127 129
|
anbi12d |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ↔ ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) ) ) |
131 |
|
vex |
⊢ 𝑦 ∈ V |
132 |
|
vex |
⊢ 𝑢 ∈ V |
133 |
131 132 2
|
sbc2ie |
⊢ ( [ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ↔ 𝜒 ) |
134 |
133
|
bicomi |
⊢ ( 𝜒 ↔ [ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ) |
135 |
134
|
a1i |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( 𝜒 ↔ [ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ) ) |
136 |
|
simpr |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) |
137 |
136
|
sbceq1d |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( [ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ) ) |
138 |
|
dfsbcq |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ 𝑢 / 𝑤 ] 𝜑 ↔ [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) |
139 |
138
|
sbcbidv |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) |
140 |
139
|
adantl |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) |
141 |
140
|
adantr |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) |
142 |
135 137 141
|
3bitrd |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( 𝜒 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) |
143 |
130 142
|
imbi12d |
⊢ ( ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ↔ ( ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) ) |
144 |
121 143
|
rspcdv |
⊢ ( ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) → ( ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) ) |
145 |
53 144
|
rspcimdv |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) → ( ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) → ( ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) ) |
146 |
88 89 120 145
|
syl3c |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) |
147 |
146 112
|
jca |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) |
148 |
|
dfsbcq |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ) ) |
149 |
|
sbccom |
⊢ ( [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) |
150 |
148 149
|
bitrdi |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) |
151 |
123
|
eqeq2d |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) |
152 |
150 151
|
anbi12d |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) ↔ ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) ) |
153 |
|
oveq1 |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( 𝑢 ++ 〈“ 𝑠 ”〉 ) = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ 𝑠 ”〉 ) ) |
154 |
153
|
sbceq1d |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ ( 𝑢 ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ) |
155 |
152 154
|
imbi12d |
⊢ ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ( ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → [ ( 𝑢 ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ) ) |
156 |
|
s1eq |
⊢ ( 𝑠 = ( lastS ‘ 𝑤 ) → 〈“ 𝑠 ”〉 = 〈“ ( lastS ‘ 𝑤 ) ”〉 ) |
157 |
156
|
oveq2d |
⊢ ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ 𝑠 ”〉 ) = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) ) |
158 |
157
|
sbceq1d |
⊢ ( 𝑠 = ( lastS ‘ 𝑤 ) → ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ) |
159 |
158
|
imbi2d |
⊢ ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ) ) |
160 |
|
sbccom |
⊢ ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ↔ [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) |
161 |
160
|
a1i |
⊢ ( 𝑠 = ( lastS ‘ 𝑤 ) → ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ↔ [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
162 |
161
|
imbi2d |
⊢ ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) ) |
163 |
159 162
|
bitrd |
⊢ ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) ) |
164 |
|
dfsbcq |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) |
165 |
|
fveqeq2 |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) |
166 |
164 165
|
anbi12d |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ↔ ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) ) |
167 |
|
oveq1 |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( 𝑦 ++ 〈“ 𝑧 ”〉 ) = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ 𝑧 ”〉 ) ) |
168 |
167
|
sbceq1d |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
169 |
166 168
|
imbi12d |
⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ↔ ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) ) |
170 |
|
s1eq |
⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → 〈“ 𝑧 ”〉 = 〈“ ( lastS ‘ 𝑥 ) ”〉 ) |
171 |
170
|
oveq2d |
⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ 𝑧 ”〉 ) = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) ) |
172 |
171
|
sbceq1d |
⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → ( [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
173 |
172
|
imbi2d |
⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → ( ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ↔ ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) ) |
174 |
|
simplr |
⊢ ( ( ( ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) |
175 |
|
simpll |
⊢ ( ( ( ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ) |
176 |
|
simpr |
⊢ ( ( ( ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) |
177 |
174 175 176 7
|
syl3anc |
⊢ ( ( ( ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝜒 → 𝜃 ) ) |
178 |
2
|
ancoms |
⊢ ( ( 𝑤 = 𝑢 ∧ 𝑥 = 𝑦 ) → ( 𝜑 ↔ 𝜒 ) ) |
179 |
132 131 178
|
sbc2ie |
⊢ ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜒 ) |
180 |
|
ovex |
⊢ ( 𝑢 ++ 〈“ 𝑠 ”〉 ) ∈ V |
181 |
|
ovex |
⊢ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) ∈ V |
182 |
3
|
ancoms |
⊢ ( ( 𝑤 = ( 𝑢 ++ 〈“ 𝑠 ”〉 ) ∧ 𝑥 = ( 𝑦 ++ 〈“ 𝑧 ”〉 ) ) → ( 𝜑 ↔ 𝜃 ) ) |
183 |
180 181 182
|
sbc2ie |
⊢ ( [ ( 𝑢 ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ↔ 𝜃 ) |
184 |
177 179 183
|
3imtr4g |
⊢ ( ( ( ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 → [ ( 𝑢 ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ) |
185 |
184
|
ex |
⊢ ( ( ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 → [ ( 𝑢 ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ) ) |
186 |
185
|
impcomd |
⊢ ( ( ( 𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → [ ( 𝑢 ++ 〈“ 𝑠 ”〉 ) / 𝑤 ] [ ( 𝑦 ++ 〈“ 𝑧 ”〉 ) / 𝑥 ] 𝜑 ) ) |
187 |
155 163 169 173 186
|
vtocl4ga |
⊢ ( ( ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ∧ ( lastS ‘ 𝑥 ) ∈ 𝑋 ) ) → ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
188 |
87 147 187
|
sylc |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) |
189 |
|
eqtr2 |
⊢ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → ( ♯ ‘ 𝑤 ) = ( 𝑚 + 1 ) ) |
190 |
189
|
ad2antll |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑤 ) = ( 𝑚 + 1 ) ) |
191 |
190 95
|
eqeltrd |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ ) |
192 |
|
wrdfin |
⊢ ( 𝑤 ∈ Word 𝑌 → 𝑤 ∈ Fin ) |
193 |
192
|
adantr |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) → 𝑤 ∈ Fin ) |
194 |
193
|
ad2antrl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ∈ Fin ) |
195 |
|
hashnncl |
⊢ ( 𝑤 ∈ Fin → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ 𝑤 ≠ ∅ ) ) |
196 |
194 195
|
syl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ 𝑤 ≠ ∅ ) ) |
197 |
191 196
|
mpbid |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ≠ ∅ ) |
198 |
|
pfxlswccat |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅ ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) = 𝑤 ) |
199 |
198
|
eqcomd |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅ ) → 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) ) |
200 |
102 197 199
|
syl2anc |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) ) |
201 |
|
wrdfin |
⊢ ( 𝑥 ∈ Word 𝑋 → 𝑥 ∈ Fin ) |
202 |
201
|
adantl |
⊢ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) → 𝑥 ∈ Fin ) |
203 |
202
|
ad2antrl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ∈ Fin ) |
204 |
|
hashnncl |
⊢ ( 𝑥 ∈ Fin → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) ) |
205 |
203 204
|
syl |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) ) |
206 |
96 205
|
mpbid |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ≠ ∅ ) |
207 |
|
pfxlswccat |
⊢ ( ( 𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅ ) → ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) = 𝑥 ) |
208 |
207
|
eqcomd |
⊢ ( ( 𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅ ) → 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) ) |
209 |
92 206 208
|
syl2anc |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) ) |
210 |
|
sbceq1a |
⊢ ( 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) → ( 𝜑 ↔ [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
211 |
|
sbceq1a |
⊢ ( 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) → ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
212 |
210 211
|
sylan9bb |
⊢ ( ( 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) ∧ 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) ) → ( 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
213 |
200 209 212
|
syl2anc |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑥 ) ”〉 ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ 〈“ ( lastS ‘ 𝑤 ) ”〉 ) / 𝑤 ] 𝜑 ) ) |
214 |
188 213
|
mpbird |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝜑 ) |
215 |
214
|
expr |
⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( 𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋 ) ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) |
216 |
215
|
ralrimivva |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) → ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) |
217 |
216
|
ex |
⊢ ( 𝑚 ∈ ℕ0 → ( ∀ 𝑢 ∈ Word 𝑌 ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) → ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) ) |
218 |
51 217
|
syl5bi |
⊢ ( 𝑚 ∈ ℕ0 → ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) → ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) ) |
219 |
12 16 20 24 41 218
|
nn0ind |
⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ) |
220 |
8 219
|
syl |
⊢ ( 𝐴 ∈ Word 𝑋 → ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ) |
221 |
220
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ) |
222 |
|
fveq2 |
⊢ ( 𝑤 = 𝐵 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝐵 ) ) |
223 |
222
|
eqeq2d |
⊢ ( 𝑤 = 𝐵 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) ) |
224 |
223
|
anbi1d |
⊢ ( 𝑤 = 𝐵 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ) ) |
225 |
224 5
|
imbi12d |
⊢ ( 𝑤 = 𝐵 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) ) |
226 |
225
|
ralbidv |
⊢ ( 𝑤 = 𝐵 → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ↔ ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) ) |
227 |
226
|
rspcv |
⊢ ( 𝐵 ∈ Word 𝑌 → ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) → ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) ) |
228 |
227
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ∀ 𝑤 ∈ Word 𝑌 ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) → ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) ) |
229 |
221 228
|
mpd |
⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) |
230 |
|
eqidd |
⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) |
231 |
|
fveqeq2 |
⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) |
232 |
|
fveqeq2 |
⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) ) |
233 |
231 232
|
anbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ↔ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) ) ) |
234 |
233 4
|
imbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ↔ ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) → 𝜏 ) ) ) |
235 |
234
|
rspcv |
⊢ ( 𝐴 ∈ Word 𝑋 → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) → 𝜏 ) ) ) |
236 |
235
|
com23 |
⊢ ( 𝐴 ∈ Word 𝑋 → ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → 𝜏 ) ) ) |
237 |
236
|
expd |
⊢ ( 𝐴 ∈ Word 𝑋 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → 𝜏 ) ) ) ) |
238 |
237
|
com34 |
⊢ ( 𝐴 ∈ Word 𝑋 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) ) ) |
239 |
238
|
imp |
⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) ) |
240 |
239
|
3adant2 |
⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) ) |
241 |
229 230 240
|
mp2d |
⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝜏 ) |