Proof of Theorem clwwlknonex2lem2
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑊 ∈ Word 𝑉) |
2 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝑉) |
3 | | elfzonn0 13432 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈
(0..^((♯‘𝑊)
− 1)) → 𝑖 ∈
ℕ0) |
4 | 3 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈
ℕ0) |
5 | | lencl 14236 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
6 | | elfzo0 13428 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(0..^((♯‘𝑊)
− 1)) ↔ (𝑖
∈ ℕ0 ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1))) |
7 | | nn0re 12242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
8 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → 𝑖 ∈ ℝ) |
9 | | nn0re 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ ℝ) |
10 | | peano2rem 11288 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑊)
∈ ℝ → ((♯‘𝑊) − 1) ∈
ℝ) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑊)
∈ ℕ0 → ((♯‘𝑊) − 1) ∈
ℝ) |
12 | 11 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → ((♯‘𝑊) − 1) ∈
ℝ) |
13 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → (♯‘𝑊) ∈ ℝ) |
14 | 8, 12, 13 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → (𝑖 ∈ ℝ ∧ ((♯‘𝑊) − 1) ∈ ℝ
∧ (♯‘𝑊)
∈ ℝ)) |
15 | 9 | ltm1d 11907 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑊)
∈ ℕ0 → ((♯‘𝑊) − 1) < (♯‘𝑊)) |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → ((♯‘𝑊) − 1) < (♯‘𝑊)) |
17 | | lttr 11051 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ℝ ∧
((♯‘𝑊) −
1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → ((𝑖 < ((♯‘𝑊) − 1) ∧
((♯‘𝑊) −
1) < (♯‘𝑊))
→ 𝑖 <
(♯‘𝑊))) |
18 | 17 | expcomd 417 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℝ ∧
((♯‘𝑊) −
1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) →
(((♯‘𝑊) −
1) < (♯‘𝑊)
→ (𝑖 <
((♯‘𝑊) −
1) → 𝑖 <
(♯‘𝑊)))) |
19 | 14, 16, 18 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → (𝑖 < ((♯‘𝑊) − 1) → 𝑖 < (♯‘𝑊))) |
20 | 19 | impancom 452 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℕ0
∧ 𝑖 <
((♯‘𝑊) −
1)) → ((♯‘𝑊) ∈ ℕ0 → 𝑖 < (♯‘𝑊))) |
21 | 20 | 3adant2 1130 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℕ0
∧ ((♯‘𝑊)
− 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0
→ 𝑖 <
(♯‘𝑊))) |
22 | 6, 21 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(0..^((♯‘𝑊)
− 1)) → ((♯‘𝑊) ∈ ℕ0 → 𝑖 < (♯‘𝑊))) |
23 | 5, 22 | syl5com 31 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝑉 → (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 < (♯‘𝑊))) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 < (♯‘𝑊))) |
25 | 24 | imp 407 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 < (♯‘𝑊)) |
26 | | ccat2s1fvw 14349 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ ℕ0 ∧ 𝑖 < (♯‘𝑊)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖) = (𝑊‘𝑖)) |
27 | 2, 4, 25, 26 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖) = (𝑊‘𝑖)) |
28 | 27 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊‘𝑖) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖)) |
29 | | peano2nn0 12273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
30 | 4, 29 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈
ℕ0) |
31 | | 1red 10976 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → 1 ∈ ℝ) |
32 | 8, 31, 13 | ltaddsubd 11575 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → ((𝑖 + 1) < (♯‘𝑊) ↔ 𝑖 < ((♯‘𝑊) − 1))) |
33 | 32 | biimprd 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0) → (𝑖 < ((♯‘𝑊) − 1) → (𝑖 + 1) < (♯‘𝑊))) |
34 | 33 | impancom 452 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℕ0
∧ 𝑖 <
((♯‘𝑊) −
1)) → ((♯‘𝑊) ∈ ℕ0 → (𝑖 + 1) < (♯‘𝑊))) |
35 | 34 | 3adant2 1130 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℕ0
∧ ((♯‘𝑊)
− 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ0
→ (𝑖 + 1) <
(♯‘𝑊))) |
36 | 6, 35 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈
(0..^((♯‘𝑊)
− 1)) → ((♯‘𝑊) ∈ ℕ0 → (𝑖 + 1) < (♯‘𝑊))) |
37 | 5, 36 | mpan9 507 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) < (♯‘𝑊)) |
38 | 37 | adantlr 712 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) < (♯‘𝑊)) |
39 | | ccat2s1fvw 14349 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (♯‘𝑊)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
40 | 2, 30, 38, 39 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
41 | 40 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊‘(𝑖 + 1)) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))) |
42 | 28, 41 | preq12d 4677 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))}) |
43 | 42 | eleq1d 2823 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
44 | 43 | ralbidva 3111 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
45 | 44 | biimpd 228 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
46 | 45 | impancom 452 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
47 | 46 | 3adant3 1131 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
48 | 47 | 3ad2ant1 1132 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
49 | 48 | com12 32 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
50 | 49 | a1dd 50 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
51 | 50 | 3adant3 1131 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ∈ Word
𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
52 | 51 | imp31 418 |
. 2
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸) |
53 | | ax-1 6 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
54 | 53 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ({𝑋, 𝑌} ∈ 𝐸 → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
55 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
𝑊 ∈ Word 𝑉) |
56 | | oveq1 7282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑊) =
(𝑁 − 2) →
((♯‘𝑊) −
1) = ((𝑁 − 2) −
1)) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝑊)
= (𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((♯‘𝑊) − 1) = ((𝑁 − 2) − 1)) |
58 | | eluzelcn 12594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
59 | | 2cnd 12051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
60 | | 1cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℂ) |
61 | 58, 59, 60 | subsub4d 11363 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1))) |
62 | | 2p1e3 12115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2 + 1) =
3 |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → (2 + 1) = 3) |
64 | 63 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3)) |
65 | | uznn0sub 12617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 3) ∈
ℕ0) |
66 | 64, 65 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 + 1)) ∈
ℕ0) |
67 | 61, 66 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) ∈
ℕ0) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝑊)
= (𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑁 − 2) − 1) ∈
ℕ0) |
69 | 57, 68 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((♯‘𝑊)
= (𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((♯‘𝑊) − 1) ∈
ℕ0) |
70 | 69 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → ((♯‘𝑊) − 1) ∈
ℕ0) |
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
((♯‘𝑊) −
1) ∈ ℕ0) |
72 | 5, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℝ) |
73 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
(♯‘𝑊) ∈
ℝ) |
74 | 73 | ltm1d 11907 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
((♯‘𝑊) −
1) < (♯‘𝑊)) |
75 | 55, 71, 74 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
(𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))) |
76 | 75 | ex 413 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2)) →
(𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)))) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2)) →
(𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)))) |
78 | 77 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → ((𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2)) →
(𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)))) |
79 | 78 | imp 407 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
(𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
ℕ0 ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))) |
80 | | ccat2s1fvw 14349 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ0
∧ ((♯‘𝑊)
− 1) < (♯‘𝑊)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1))) |
82 | | nn0cn 12243 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ ℂ) |
83 | | ax-1cn 10929 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ |
84 | | npcan 11230 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑊)
∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑊) − 1) + 1) =
(♯‘𝑊)) |
85 | 82, 83, 84 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑊)
∈ ℕ0 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊)) |
86 | 5, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ Word 𝑉 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊)) |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊)) |
88 | 87 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊)) |
89 | 88 | fveq2d 6778 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1)) = (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(♯‘𝑊))) |
90 | | simp1l 1196 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → 𝑊 ∈ Word 𝑉) |
91 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (♯‘𝑊) = (♯‘𝑊)) |
92 | | simp2l 1198 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → 𝑋 ∈ 𝑉) |
93 | | ccatw2s1p1 14346 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ 𝑋 ∈ 𝑉) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)) = 𝑋) |
94 | 90, 91, 92, 93 | syl3anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)) = 𝑋) |
95 | 89, 94 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1)) = 𝑋) |
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1)) = 𝑋) |
97 | 81, 96 | preq12d 4677 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
{(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} = {(𝑊‘((♯‘𝑊) − 1)), 𝑋}) |
98 | | lsw 14267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
99 | 98 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
100 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘0) = 𝑋) |
101 | 99, 100 | preq12d 4677 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → {(lastS‘𝑊), (𝑊‘0)} = {(𝑊‘((♯‘𝑊) − 1)), 𝑋}) |
102 | 101 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 ↔ {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)) |
103 | 102 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)) |
104 | 103 | expcom 414 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊‘0) = 𝑋 → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸))) |
105 | 104 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝑉 → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → ((𝑊‘0) = 𝑋 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸))) |
106 | 105 | imp31 418 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸) |
107 | 106 | 3adant2 1130 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸) |
108 | 107 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
{(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸) |
109 | 97, 108 | eqeltrd 2839 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (♯‘𝑊) =
(𝑁 − 2))) →
{(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸) |
110 | 109 | exp520 1356 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → (𝑁 ∈ (ℤ≥‘3)
→ ((♯‘𝑊) =
(𝑁 − 2) →
{(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))))) |
111 | 110 | com14 96 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))))) |
112 | 111 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))))) |
113 | 54, 112 | syld 47 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ({𝑋, 𝑌} ∈ 𝐸 → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))))) |
114 | 113 | com25 99 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((♯‘𝑊) =
(𝑁 − 2) →
((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))))) |
115 | 114 | com14 96 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))))) |
116 | 115 | 3adant2 1130 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))))) |
117 | 116 | 3imp 1110 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))) |
118 | 117 | impcom 408 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)) |
119 | 118 | imp 407 |
. . 3
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸) |
120 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (♯‘𝑊) = (♯‘𝑊)) |
121 | | simprl 768 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑋 ∈ 𝑉) |
122 | 1, 120, 121, 93 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)) = 𝑋) |
123 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(♯‘𝑊) =
(♯‘𝑊) |
124 | | ccatw2s1p2 14348 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1)) = 𝑌) |
125 | 123, 124 | mpanl2 698 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1)) = 𝑌) |
126 | 122, 125 | preq12d 4677 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}) |
127 | 126 | expcom 414 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})) |
128 | 127 | a1i 11 |
. . . . . . . . . 10
⊢ ({𝑋, 𝑌} ∈ 𝐸 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))) |
129 | 128 | com13 88 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))) |
130 | 129 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))) |
131 | 130 | 3ad2ant1 1132 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))) |
132 | 131 | com12 32 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))) |
133 | 132 | 3adant3 1131 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ∈ Word
𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))) |
134 | 133 | imp31 418 |
. . . 4
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}) |
135 | | simpr 485 |
. . . 4
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {𝑋, 𝑌} ∈ 𝐸) |
136 | 134, 135 | eqeltrd 2839 |
. . 3
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} ∈ 𝐸) |
137 | | ovex 7308 |
. . . 4
⊢
((♯‘𝑊)
− 1) ∈ V |
138 | | fvex 6787 |
. . . 4
⊢
(♯‘𝑊)
∈ V |
139 | | fveq2 6774 |
. . . . . 6
⊢ (𝑖 = ((♯‘𝑊) − 1) → (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1))) |
140 | | fvoveq1 7298 |
. . . . . 6
⊢ (𝑖 = ((♯‘𝑊) − 1) → (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(𝑖 + 1)) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(((♯‘𝑊) − 1) +
1))) |
141 | 139, 140 | preq12d 4677 |
. . . . 5
⊢ (𝑖 = ((♯‘𝑊) − 1) → {(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} = {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) +
1))}) |
142 | 141 | eleq1d 2823 |
. . . 4
⊢ (𝑖 = ((♯‘𝑊) − 1) → ({(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)) |
143 | | fveq2 6774 |
. . . . . 6
⊢ (𝑖 = (♯‘𝑊) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊))) |
144 | | fvoveq1 7298 |
. . . . . 6
⊢ (𝑖 = (♯‘𝑊) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1)) = (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))) |
145 | 143, 144 | preq12d 4677 |
. . . . 5
⊢ (𝑖 = (♯‘𝑊) → {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} = {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))}) |
146 | 145 | eleq1d 2823 |
. . . 4
⊢ (𝑖 = (♯‘𝑊) → ({(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} ∈ 𝐸)) |
147 | 137, 138,
142, 146 | ralpr 4636 |
. . 3
⊢
(∀𝑖 ∈
{((♯‘𝑊) −
1), (♯‘𝑊)}
{(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) − 1)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(♯‘𝑊)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((♯‘𝑊) + 1))} ∈ 𝐸)) |
148 | 119, 136,
147 | sylanbrc 583 |
. 2
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸) |
149 | | ralunb 4125 |
. 2
⊢
(∀𝑖 ∈
((0..^((♯‘𝑊)
− 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
150 | 52, 148, 149 | sylanbrc 583 |
1
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪
{((♯‘𝑊) −
1), (♯‘𝑊)}){(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸) |