Proof of Theorem numclwlk2lem2f
Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | | 2nn0 11186 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
3 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) |
4 | 1, 3 | nn0addcld 11232 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
ℕ0) |
5 | 4 | anim2i 591 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈
ℕ0)) |
6 | 5 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈
ℕ0)) |
7 | | numclwwlk.c |
. . . . . . . . 9
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
8 | | numclwwlk.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
9 | | numclwwlk.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
10 | | numclwwlk.q |
. . . . . . . . 9
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
11 | | numclwwlk.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
12 | 7, 8, 9, 10, 11 | numclwwlkovh 26628 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ0) →
(𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) |
13 | 12 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ0) →
(𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})) |
14 | 6, 13 | syl 17 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})) |
15 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0)) |
16 | 15 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((𝑤‘0) = 𝑋 ↔ (𝑥‘0) = 𝑋)) |
17 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤‘((𝑁 + 2) − 2)) = (𝑥‘((𝑁 + 2) − 2))) |
18 | 17, 15 | neeq12d 2843 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) |
19 | 16, 18 | anbi12d 743 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) |
20 | 19 | elrab 3331 |
. . . . . 6
⊢ (𝑥 ∈ {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ (𝑥 ∈ (𝐶‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) |
21 | 14, 20 | syl6bb 275 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ (𝐶‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) |
22 | 4 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) ∈
ℕ0) |
23 | 7 | numclwwlkfvc 26604 |
. . . . . . . . 9
⊢ ((𝑁 + 2) ∈ ℕ0
→ (𝐶‘(𝑁 + 2)) = ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2))) |
24 | 23 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑁 + 2) ∈ ℕ0
→ (𝑥 ∈ (𝐶‘(𝑁 + 2)) ↔ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)))) |
25 | 22, 24 | syl 17 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝐶‘(𝑁 + 2)) ↔ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)))) |
26 | 25 | anbi1d 737 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑥 ∈ (𝐶‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) |
27 | | peano2nn 10909 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
28 | | nnz 11276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
29 | | 2z 11286 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 2 ∈
ℤ) |
31 | 28, 30 | zaddcld 11362 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
ℤ) |
32 | | uzid 11578 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 2) ∈ ℤ →
(𝑁 + 2) ∈
(ℤ≥‘(𝑁 + 2))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
(ℤ≥‘(𝑁 + 2))) |
34 | | nncn 10905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
35 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
36 | 34, 35, 35 | addassd 9941 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1))) |
37 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 1) =
2 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (1 + 1) =
2) |
39 | 38 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (𝑁 + (1 + 1)) = (𝑁 + 2)) |
40 | 36, 39 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + 2)) |
41 | 40 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘((𝑁 + 1) + 1)) =
(ℤ≥‘(𝑁 + 2))) |
42 | 33, 41 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
(ℤ≥‘((𝑁 + 1) + 1))) |
43 | 27, 42 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧
(𝑁 + 2) ∈
(ℤ≥‘((𝑁 + 1) + 1)))) |
44 | 43 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑁 + 1) ∈ ℕ ∧ (𝑁 + 2) ∈
(ℤ≥‘((𝑁 + 1) + 1)))) |
45 | 44 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → ((𝑁 + 1) ∈ ℕ ∧ (𝑁 + 2) ∈
(ℤ≥‘((𝑁 + 1) + 1)))) |
46 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2))) |
47 | | wwlksubclwwlk 26332 |
. . . . . . . . . 10
⊢ (((𝑁 + 1) ∈ ℕ ∧
(𝑁 + 2) ∈
(ℤ≥‘((𝑁 + 1) + 1))) → (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘((𝑁 + 1) − 1)))) |
48 | 45, 46, 47 | sylc 63 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘((𝑁 + 1) − 1))) |
49 | | pncan1 10333 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
50 | 49 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → 𝑁 = ((𝑁 + 1) − 1)) |
51 | 34, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1)) |
52 | 51 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑉 WWalksN 𝐸)‘𝑁) = ((𝑉 WWalksN 𝐸)‘((𝑁 + 1) − 1))) |
53 | 52 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘((𝑁 + 1) − 1)))) |
54 | 53 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘((𝑁 + 1) − 1)))) |
55 | 54 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘((𝑁 + 1) − 1)))) |
56 | 48, 55 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
57 | | clwwlknprop 26300 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ ((𝑁 + 2) ∈ ℕ0 ∧
(#‘𝑥) = (𝑁 + 2)))) |
58 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (𝑥‘0) = 𝑋) |
59 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → 𝑥 ∈ Word 𝑉) |
60 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
61 | 1, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) |
62 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
63 | 62 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1)) |
64 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ (0...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ0
∧ 𝑁 ≤ (𝑁 + 1))) |
65 | 1, 61, 63, 64 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...(𝑁 + 1))) |
66 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
67 | | addsubass 10170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 2) − 1) = (𝑁 + (2 − 1))) |
68 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (2
− 1) = 1 |
69 | 68 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 + (2 − 1)) = (𝑁 + 1) |
70 | 67, 69 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 2) − 1) = (𝑁 + 1)) |
71 | 34, 66, 35, 70 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ → ((𝑁 + 2) − 1) = (𝑁 + 1)) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℕ →
(0...((𝑁 + 2) − 1)) =
(0...(𝑁 +
1))) |
73 | 65, 72 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...((𝑁 + 2) − 1))) |
74 | | elfzp1b 12286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 + 2) ∈ ℤ) →
(𝑁 ∈ (0...((𝑁 + 2) − 1)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 2)))) |
75 | 28, 31, 74 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ (0...((𝑁 + 2) − 1)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 2)))) |
76 | 73, 75 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (1...(𝑁 + 2))) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑁 + 1) ∈ (1...(𝑁 + 2))) |
78 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝑥) =
(𝑁 + 2) →
(1...(#‘𝑥)) =
(1...(𝑁 +
2))) |
79 | 78 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑥) =
(𝑁 + 2) → ((𝑁 + 1) ∈ (1...(#‘𝑥)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 2)))) |
80 | 79 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → ((𝑁 + 1) ∈ (1...(#‘𝑥)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 2)))) |
81 | 77, 80 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑁 + 1) ∈ (1...(#‘𝑥))) |
82 | | swrd0fv0 13292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑥))) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
83 | 59, 81, 82 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
84 | 83 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ →
(((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0))) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0))) |
86 | 85 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
87 | 86 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥‘0) = 𝑋 ∧ ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
88 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥‘0) = 𝑋 ∧ ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → (𝑥‘0) = 𝑋) |
89 | 87, 88 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥‘0) = 𝑋 ∧ ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋) |
90 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑥))) → ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) = (𝑥‘((𝑁 + 1) − 1))) |
91 | 59, 81, 90 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) = (𝑥‘((𝑁 + 1) − 1))) |
92 | 34, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
93 | 34, 66 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℕ → ((𝑁 + 2) − 2) = 𝑁) |
94 | 92, 93 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = ((𝑁 + 2) −
2)) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ → (𝑥‘((𝑁 + 1) − 1)) = (𝑥‘((𝑁 + 2) − 2))) |
96 | 95 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑥‘((𝑁 + 1) − 1)) = (𝑥‘((𝑁 + 2) − 2))) |
97 | 91, 96 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℕ ∧
((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑥‘((𝑁 + 2) − 2)) = ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉))) |
98 | 97 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ →
(((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥‘((𝑁 + 2) − 2)) = ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)))) |
99 | 98 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥‘((𝑁 + 2) − 2)) = ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)))) |
100 | 99 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥‘((𝑁 + 2) − 2)) = ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉))) |
101 | 100 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0) ↔ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ (𝑥‘0))) |
102 | 101 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0) → ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ( lastS
‘(𝑥 substr 〈0,
(𝑁 + 1)〉)) ≠ (𝑥‘0))) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ( lastS
‘(𝑥 substr 〈0,
(𝑁 + 1)〉)) ≠ (𝑥‘0))) |
104 | 103 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ (𝑥‘0)) |
105 | 104 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥‘0) = 𝑋 ∧ ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ (𝑥‘0)) |
106 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑋 = (𝑥‘0) → (( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋 ↔ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ (𝑥‘0))) |
107 | 106 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥‘0) = 𝑋 → (( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋 ↔ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ (𝑥‘0))) |
108 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥‘0) = 𝑋 ∧ ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → (( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋 ↔ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ (𝑥‘0))) |
109 | 105, 108 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥‘0) = 𝑋 ∧ ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋) |
110 | 89, 109 | jca 553 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥‘0) = 𝑋 ∧ ((((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)) |
111 | 58, 110 | mpancom 700 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)) |
112 | 111 | exp31 628 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
113 | 112 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
114 | 113 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑥) =
(𝑁 + 2) → (𝑥 ∈ Word 𝑉 → (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))))) |
115 | 114 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 + 2) ∈ ℕ0
∧ (#‘𝑥) = (𝑁 + 2)) → (𝑥 ∈ Word 𝑉 → (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))))) |
116 | 115 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((𝑁 + 2) ∈ ℕ0 ∧
(#‘𝑥) = (𝑁 + 2))) → (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
117 | 116 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ ((𝑁 + 2) ∈ ℕ0 ∧
(#‘𝑥) = (𝑁 + 2))) → (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
118 | 57, 117 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) → (((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
119 | 118 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))) |
120 | 119 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))) |
121 | 120 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))) |
122 | 121 | imp 444 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)) |
123 | 56, 122 | jca 553 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))) |
124 | 123 | ex 449 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
125 | 26, 124 | sylbid 229 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑥 ∈ (𝐶‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
126 | 21, 125 | sylbid 229 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
127 | 126 | imp 444 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))) |
128 | 1 | anim2i 591 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
129 | 128 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
130 | 129 | adantr 480 |
. . . . . 6
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
131 | 7, 8, 9, 10 | numclwwlkovq 26626 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋𝑄𝑁) = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
132 | 130, 131 | syl 17 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑋𝑄𝑁) = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
133 | 132 | eleq2d 2673 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ (𝑋𝑄𝑁) ↔ (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)})) |
134 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑤 = (𝑥 substr 〈0, (𝑁 + 1)〉) → (𝑤‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
135 | 134 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑤 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ((𝑤‘0) = 𝑋 ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋)) |
136 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ( lastS ‘𝑤) = ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉))) |
137 | 136 | neeq1d 2841 |
. . . . . 6
⊢ (𝑤 = (𝑥 substr 〈0, (𝑁 + 1)〉) → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)) |
138 | 135, 137 | anbi12d 743 |
. . . . 5
⊢ (𝑤 = (𝑥 substr 〈0, (𝑁 + 1)〉) → (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) ↔ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))) |
139 | 138 | elrab 3331 |
. . . 4
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋))) |
140 | 133, 139 | syl6bb 275 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ (𝑋𝑄𝑁) ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑋 ∧ ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)) ≠ 𝑋)))) |
141 | 127, 140 | mpbird 246 |
. 2
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ (𝑋𝑄𝑁)) |
142 | | numclwwlk.r |
. 2
⊢ 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 substr 〈0, (𝑁 + 1)〉)) |
143 | 141, 142 | fmptd 6292 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))⟶(𝑋𝑄𝑁)) |