Step | Hyp | Ref
| Expression |
1 | | 1nn0 11308 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
2 | | iswwlksn 26730 |
. . . . . . . . 9
⊢ (1 ∈
ℕ0 → (𝑤 ∈ (1 WWalksN 𝐺) ↔ (𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (1 + 1)))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑤 ∈ (1 WWalksN 𝐺) ↔ (𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (1 + 1))) |
4 | | rusgrnumwwlkl1.v |
. . . . . . . . . 10
⊢ 𝑉 = (Vtx‘𝐺) |
5 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
6 | 4, 5 | iswwlks 26728 |
. . . . . . . . 9
⊢ (𝑤 ∈ (WWalks‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
7 | 6 | anbi1i 731 |
. . . . . . . 8
⊢ ((𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (1 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1))) |
8 | 3, 7 | bitri 264 |
. . . . . . 7
⊢ (𝑤 ∈ (1 WWalksN 𝐺) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1))) |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (𝑤 ∈ (1 WWalksN 𝐺) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1)))) |
10 | 9 | anbi1d 741 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ (1 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃) ↔ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃))) |
11 | | 1p1e2 11134 |
. . . . . . . . . . 11
⊢ (1 + 1) =
2 |
12 | 11 | eqeq2i 2634 |
. . . . . . . . . 10
⊢
((#‘𝑤) = (1 +
1) ↔ (#‘𝑤) =
2) |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((#‘𝑤) = (1 + 1) ↔ (#‘𝑤) = 2)) |
14 | 13 | anbi2d 740 |
. . . . . . . 8
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = 2))) |
15 | | 3anass 1042 |
. . . . . . . . . . . 12
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
17 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ∅ → (#‘𝑤) =
(#‘∅)) |
18 | | hash0 13158 |
. . . . . . . . . . . . . . . 16
⊢
(#‘∅) = 0 |
19 | 17, 18 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ∅ → (#‘𝑤) = 0) |
20 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 |
21 | 20 | nesymi 2851 |
. . . . . . . . . . . . . . . 16
⊢ ¬ 0
= 2 |
22 | | eqeq1 2626 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 0
→ ((#‘𝑤) = 2
↔ 0 = 2)) |
23 | 21, 22 | mtbiri 317 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 0
→ ¬ (#‘𝑤) =
2) |
24 | 19, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∅ → ¬
(#‘𝑤) =
2) |
25 | 24 | necon2ai 2823 |
. . . . . . . . . . . . 13
⊢
((#‘𝑤) = 2
→ 𝑤 ≠
∅) |
26 | 25 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → 𝑤 ≠ ∅) |
27 | 26 | biantrurd 529 |
. . . . . . . . . . 11
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
28 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) = 2
→ ((#‘𝑤) −
1) = (2 − 1)) |
29 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
30 | 28, 29 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 2
→ ((#‘𝑤) −
1) = 1) |
31 | 30 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 2
→ (0..^((#‘𝑤)
− 1)) = (0..^1)) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → (0..^((#‘𝑤) − 1)) =
(0..^1)) |
33 | 32 | raleqdv 3144 |
. . . . . . . . . . . . 13
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
34 | | fzo01 12550 |
. . . . . . . . . . . . . . 15
⊢ (0..^1) =
{0} |
35 | 34 | raleqi 3142 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ {0} {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
36 | | c0ex 10034 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
37 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 0 → (𝑤‘𝑖) = (𝑤‘0)) |
38 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
39 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 + 1) =
1 |
40 | 38, 39 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 0 → (𝑖 + 1) = 1) |
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 0 → (𝑤‘(𝑖 + 1)) = (𝑤‘1)) |
42 | 37, 41 | preq12d 4276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 0 → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘0), (𝑤‘1)}) |
43 | 42 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 0 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
44 | 36, 43 | ralsn 4222 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
{0} {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) |
45 | 35, 44 | bitri 264 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
(0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) |
46 | 33, 45 | syl6bb 276 |
. . . . . . . . . . . 12
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
47 | 46 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))) |
48 | 16, 27, 47 | 3bitr2d 296 |
. . . . . . . . . 10
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))) |
49 | 48 | ex 450 |
. . . . . . . . 9
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((#‘𝑤) = 2 → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))))) |
50 | 49 | pm5.32rd 672 |
. . . . . . . 8
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = 2) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = 2))) |
51 | 14, 50 | bitrd 268 |
. . . . . . 7
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1)) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = 2))) |
52 | 51 | anbi1d 741 |
. . . . . 6
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = 2) ∧ (𝑤‘0) = 𝑃))) |
53 | | anass 681 |
. . . . . 6
⊢ ((((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = 2) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃))) |
54 | 52, 53 | syl6bb 276 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)))) |
55 | | anass 681 |
. . . . . . 7
⊢ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)))) |
56 | | ancom 466 |
. . . . . . . . 9
⊢ (({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
57 | | df-3an 1039 |
. . . . . . . . 9
⊢
(((#‘𝑤) = 2
∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ↔ (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
58 | 56, 57 | bitr4i 267 |
. . . . . . . 8
⊢ (({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
59 | 58 | anbi2i 730 |
. . . . . . 7
⊢ ((𝑤 ∈ Word 𝑉 ∧ ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃))) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))) |
60 | 55, 59 | bitri 264 |
. . . . . 6
⊢ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))) |
61 | 60 | a1i 11 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))))) |
62 | 10, 54, 61 | 3bitrd 294 |
. . . 4
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ (1 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))))) |
63 | 62 | rabbidva2 3186 |
. . 3
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → {𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}) |
64 | 63 | fveq2d 6195 |
. 2
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (#‘{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))})) |
65 | 4 | rusgrnumwrdl2 26482 |
. 2
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}) = 𝐾) |
66 | 64, 65 | eqtrd 2656 |
1
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = 𝐾) |