Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺)) → (𝑊 substr 〈0, (𝑁 + 1)〉) = (𝑊 substr 〈0, (𝑁 + 1)〉)) |
2 | | eqid 2610 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | wwlksnredwwlkn.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
4 | 2, 3 | wwlknp 41045 |
. . . 4
⊢ (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
5 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1))) → 𝑊 ∈ Word (Vtx‘𝐺)) |
6 | | peano2nn0 11210 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
7 | | peano2nn0 11210 |
. . . . . . . . . . . . 13
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
9 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
10 | | nn0p1nn 11209 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ) |
11 | 6, 10 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ) |
12 | | nn0re 11178 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
13 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) |
14 | | peano2re 10088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
15 | | peano2re 10088 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 + 1) ∈ ℝ →
((𝑁 + 1) + 1) ∈
ℝ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℝ → ((𝑁 + 1) + 1) ∈
ℝ) |
17 | 13, 14, 16 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℝ → (𝑁 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ ∧
((𝑁 + 1) + 1) ∈
ℝ)) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℝ
∧ (𝑁 + 1) ∈
ℝ ∧ ((𝑁 + 1) + 1)
∈ ℝ)) |
19 | 12 | ltp1d 10833 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑁 < (𝑁 + 1)) |
20 | | nn0re 11178 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
21 | 6, 20 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
22 | 21 | ltp1d 10833 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) < ((𝑁 + 1) + 1)) |
23 | | lttr 9993 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ ∧
((𝑁 + 1) + 1) ∈
ℝ) → ((𝑁 <
(𝑁 + 1) ∧ (𝑁 + 1) < ((𝑁 + 1) + 1)) → 𝑁 < ((𝑁 + 1) + 1))) |
24 | 23 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ ∧
((𝑁 + 1) + 1) ∈
ℝ) ∧ (𝑁 <
(𝑁 + 1) ∧ (𝑁 + 1) < ((𝑁 + 1) + 1))) → 𝑁 < ((𝑁 + 1) + 1)) |
25 | 18, 19, 22, 24 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 < ((𝑁 + 1) + 1)) |
26 | | elfzo0 12376 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (0..^((𝑁 + 1) + 1)) ↔ (𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) + 1) ∈ ℕ ∧
𝑁 < ((𝑁 + 1) + 1))) |
27 | 9, 11, 25, 26 | syl3anbrc 1239 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(0..^((𝑁 + 1) +
1))) |
28 | | fargshiftlem 26162 |
. . . . . . . . . . . 12
⊢ ((((𝑁 + 1) + 1) ∈
ℕ0 ∧ 𝑁
∈ (0..^((𝑁 + 1) + 1)))
→ (𝑁 + 1) ∈
(1...((𝑁 + 1) +
1))) |
29 | 8, 27, 28 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(1...((𝑁 + 1) +
1))) |
30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑁 + 1) ∈ (1...((𝑁 + 1) + 1))) |
31 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
(1...(#‘𝑊)) =
(1...((𝑁 + 1) +
1))) |
32 | 31 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ∈
(1...(#‘𝑊)) ↔
(𝑁 + 1) ∈ (1...((𝑁 + 1) + 1)))) |
33 | 32 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → ((𝑁 + 1) ∈ (1...(#‘𝑊)) ↔ (𝑁 + 1) ∈ (1...((𝑁 + 1) + 1)))) |
34 | 33 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1))) → ((𝑁 + 1) ∈ (1...(#‘𝑊)) ↔ (𝑁 + 1) ∈ (1...((𝑁 + 1) + 1)))) |
35 | 30, 34 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑁 + 1) ∈ (1...(#‘𝑊))) |
36 | 5, 35 | jca 553 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
37 | 36 | 3adantr3 1215 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
38 | | swrd0fvlsw 13295 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑊‘((𝑁 + 1) − 1))) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → ( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑊‘((𝑁 + 1) − 1))) |
40 | | lsw 13204 |
. . . . . . . 8
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
41 | 40 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
42 | 41 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
43 | 39, 42 | preq12d 4220 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} = {(𝑊‘((𝑁 + 1) − 1)), (𝑊‘((#‘𝑊) − 1))}) |
44 | | oveq1 6556 |
. . . . . . . . . . 11
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((#‘𝑊) − 1) =
(((𝑁 + 1) + 1) −
1)) |
45 | 44 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((#‘𝑊) − 1) = (((𝑁 + 1) + 1) − 1)) |
46 | 45 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → ((#‘𝑊) − 1) = (((𝑁 + 1) + 1) − 1)) |
47 | 46 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → (𝑊‘((#‘𝑊) − 1)) = (𝑊‘(((𝑁 + 1) + 1) − 1))) |
48 | 47 | preq2d 4219 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → {(𝑊‘((𝑁 + 1) − 1)), (𝑊‘((#‘𝑊) − 1))} = {(𝑊‘((𝑁 + 1) − 1)), (𝑊‘(((𝑁 + 1) + 1) − 1))}) |
49 | | nn0cn 11179 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
50 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
51 | 49, 50 | pncand 10272 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
52 | 51 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑊‘((𝑁 + 1) − 1)) = (𝑊‘𝑁)) |
53 | 6 | nn0cnd 11230 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
54 | 53, 50 | pncand 10272 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
55 | 54 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑊‘(((𝑁 + 1) + 1) − 1)) = (𝑊‘(𝑁 + 1))) |
56 | 52, 55 | preq12d 4220 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ {(𝑊‘((𝑁 + 1) − 1)), (𝑊‘(((𝑁 + 1) + 1) − 1))} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
57 | 56 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → {(𝑊‘((𝑁 + 1) − 1)), (𝑊‘(((𝑁 + 1) + 1) − 1))} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
58 | 48, 57 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → {(𝑊‘((𝑁 + 1) − 1)), (𝑊‘((#‘𝑊) − 1))} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
59 | | fzonn0p1 12411 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
60 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → (𝑊‘𝑖) = (𝑊‘𝑁)) |
61 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑁 → (𝑖 + 1) = (𝑁 + 1)) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → (𝑊‘(𝑖 + 1)) = (𝑊‘(𝑁 + 1))) |
63 | 60, 62 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑁 → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
64 | 63 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑁 → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
65 | 64 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (0..^(𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
66 | 59, 65 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
67 | 66 | com12 32 |
. . . . . . . 8
⊢
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → (𝑁 ∈ ℕ0 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
68 | 67 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (𝑁 ∈ ℕ0 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
69 | 68 | impcom 445 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸) |
70 | 58, 69 | eqeltrd 2688 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → {(𝑊‘((𝑁 + 1) − 1)), (𝑊‘((#‘𝑊) − 1))} ∈ 𝐸) |
71 | 43, 70 | eqeltrd 2688 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) → {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} ∈ 𝐸) |
72 | 4, 71 | sylan2 490 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺)) → {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} ∈ 𝐸) |
73 | | wwlksnred 41098 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalkSN 𝐺))) |
74 | 73 | imp 444 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalkSN 𝐺)) |
75 | | eqeq2 2621 |
. . . . . 6
⊢ (𝑦 = (𝑊 substr 〈0, (𝑁 + 1)〉) → ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ↔ (𝑊 substr 〈0, (𝑁 + 1)〉) = (𝑊 substr 〈0, (𝑁 + 1)〉))) |
76 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = (𝑊 substr 〈0, (𝑁 + 1)〉) → ( lastS ‘𝑦) = ( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉))) |
77 | 76 | preq1d 4218 |
. . . . . . 7
⊢ (𝑦 = (𝑊 substr 〈0, (𝑁 + 1)〉) → {( lastS ‘𝑦), ( lastS ‘𝑊)} = {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑊)}) |
78 | 77 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 = (𝑊 substr 〈0, (𝑁 + 1)〉) → ({( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ 𝐸 ↔ {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} ∈ 𝐸)) |
79 | 75, 78 | anbi12d 743 |
. . . . 5
⊢ (𝑦 = (𝑊 substr 〈0, (𝑁 + 1)〉) → (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ 𝐸) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) = (𝑊 substr 〈0, (𝑁 + 1)〉) ∧ {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸))) |
80 | 79 | adantl 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺)) ∧ 𝑦 = (𝑊 substr 〈0, (𝑁 + 1)〉)) → (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ 𝐸) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) = (𝑊 substr 〈0, (𝑁 + 1)〉) ∧ {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸))) |
81 | 74, 80 | rspcedv 3286 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺)) → (((𝑊 substr 〈0, (𝑁 + 1)〉) = (𝑊 substr 〈0, (𝑁 + 1)〉) ∧ {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸) → ∃𝑦 ∈ (𝑁 WWalkSN 𝐺)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ 𝐸))) |
82 | 1, 72, 81 | mp2and 711 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺)) → ∃𝑦 ∈ (𝑁 WWalkSN 𝐺)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ 𝐸)) |
83 | 82 | ex 449 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → ∃𝑦 ∈ (𝑁 WWalkSN 𝐺)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ 𝐸))) |