Step | Hyp | Ref
| Expression |
1 | | rusisusgra 26458 |
. . . . . . . . . 10
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
2 | | usgrav 25867 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | | 1nn0 11185 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝑃 ∈ 𝑉 → 1 ∈
ℕ0) |
6 | 3, 5 | anim12i 588 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 1 ∈
ℕ0)) |
7 | | df-3an 1033 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 1 ∈
ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 1 ∈
ℕ0)) |
8 | 6, 7 | sylibr 223 |
. . . . . . 7
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 1 ∈
ℕ0)) |
9 | | iswwlkn 26212 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 1 ∈
ℕ0) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ↔ (𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (1 + 1)))) |
10 | | iswwlk 26211 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
11 | 10 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 1 ∈
ℕ0) → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
12 | 11 | anbi1d 737 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 1 ∈
ℕ0) → ((𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (1 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)))) |
13 | 9, 12 | bitrd 267 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 1 ∈
ℕ0) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)))) |
14 | 8, 13 | syl 17 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)))) |
15 | 14 | anbi1d 737 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ∧ (𝑤‘0) = 𝑃) ↔ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃))) |
16 | | 1p1e2 11011 |
. . . . . . . . . . 11
⊢ (1 + 1) =
2 |
17 | 16 | eqeq2i 2622 |
. . . . . . . . . 10
⊢
((#‘𝑤) = (1 +
1) ↔ (#‘𝑤) =
2) |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((#‘𝑤) = (1 + 1) ↔ (#‘𝑤) = 2)) |
19 | 18 | anbi2d 736 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = 2))) |
20 | | 3anass 1035 |
. . . . . . . . . . . 12
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)))) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ∅ → (#‘𝑤) =
(#‘∅)) |
23 | | hash0 13019 |
. . . . . . . . . . . . . . . 16
⊢
(#‘∅) = 0 |
24 | 22, 23 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ∅ → (#‘𝑤) = 0) |
25 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 |
26 | 25 | nesymi 2839 |
. . . . . . . . . . . . . . . 16
⊢ ¬ 0
= 2 |
27 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 0
→ ((#‘𝑤) = 2
↔ 0 = 2)) |
28 | 26, 27 | mtbiri 316 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 0
→ ¬ (#‘𝑤) =
2) |
29 | 24, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∅ → ¬
(#‘𝑤) =
2) |
30 | 29 | necon2ai 2811 |
. . . . . . . . . . . . 13
⊢
((#‘𝑤) = 2
→ 𝑤 ≠
∅) |
31 | 30 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → 𝑤 ≠ ∅) |
32 | 31 | biantrurd 528 |
. . . . . . . . . . 11
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)))) |
33 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) = 2
→ ((#‘𝑤) −
1) = (2 − 1)) |
34 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
35 | 33, 34 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 2
→ ((#‘𝑤) −
1) = 1) |
36 | 35 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 2
→ (0..^((#‘𝑤)
− 1)) = (0..^1)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → (0..^((#‘𝑤) − 1)) =
(0..^1)) |
38 | 37 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
39 | | fzo01 12417 |
. . . . . . . . . . . . . . 15
⊢ (0..^1) =
{0} |
40 | 39 | raleqi 3119 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ {0} {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) |
41 | | c0ex 9913 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
42 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 0 → (𝑤‘𝑖) = (𝑤‘0)) |
43 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
44 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 + 1) =
1 |
45 | 43, 44 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 0 → (𝑖 + 1) = 1) |
46 | 45 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 0 → (𝑤‘(𝑖 + 1)) = (𝑤‘1)) |
47 | 42, 46 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 0 → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘0), (𝑤‘1)}) |
48 | 47 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 0 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)) |
49 | 41, 48 | ralsn 4169 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
{0} {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) |
50 | 40, 49 | bitri 263 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
(0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) |
51 | 38, 50 | syl6bb 275 |
. . . . . . . . . . . 12
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)) |
52 | 51 | anbi2d 736 |
. . . . . . . . . . 11
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸))) |
53 | 21, 32, 52 | 3bitr2d 295 |
. . . . . . . . . 10
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (#‘𝑤) = 2) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸))) |
54 | 53 | ex 449 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((#‘𝑤) = 2 → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)))) |
55 | 54 | pm5.32rd 670 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = 2) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ (#‘𝑤) = 2))) |
56 | 19, 55 | bitrd 267 |
. . . . . . 7
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ (#‘𝑤) = 2))) |
57 | 56 | anbi1d 737 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ (#‘𝑤) = 2) ∧ (𝑤‘0) = 𝑃))) |
58 | | anass 679 |
. . . . . 6
⊢ ((((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ (#‘𝑤) = 2) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃))) |
59 | 57, 58 | syl6bb 275 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)))) |
60 | | anass 679 |
. . . . . . 7
⊢ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ({(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)))) |
61 | | ancom 465 |
. . . . . . . . 9
⊢ (({(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃) ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)) |
62 | | df-3an 1033 |
. . . . . . . . 9
⊢
(((#‘𝑤) = 2
∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ↔ (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃) ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)) |
63 | 61, 62 | bitr4i 266 |
. . . . . . . 8
⊢ (({(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)) |
64 | 63 | anbi2i 726 |
. . . . . . 7
⊢ ((𝑤 ∈ Word 𝑉 ∧ ({(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃))) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸))) |
65 | 60, 64 | bitri 263 |
. . . . . 6
⊢ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸))) |
66 | 65 | a1i 11 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸) ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)))) |
67 | 15, 59, 66 | 3bitrd 293 |
. . . 4
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ∧ (𝑤‘0) = 𝑃) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)))) |
68 | 67 | rabbidva2 3162 |
. . 3
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)}) |
69 | 68 | fveq2d 6107 |
. 2
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ∣ (𝑤‘0) = 𝑃}) = (#‘{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)})) |
70 | | rusgranumwwlkl1 26473 |
. 2
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)}) = 𝐾) |
71 | 69, 70 | eqtrd 2644 |
1
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ∣ (𝑤‘0) = 𝑃}) = 𝐾) |