Step | Hyp | Ref
| Expression |
1 | | rusisusgra 26458 |
. . 3
⊢
(〈𝑉, 𝐸〉 RegUSGrph 0 → 𝑉 USGrph 𝐸) |
2 | | id 22 |
. . 3
⊢ (𝑃 ∈ 𝑉 → 𝑃 ∈ 𝑉) |
3 | | nnnn0 11176 |
. . 3
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
4 | | rusgranumwlk.w |
. . . 4
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛}) |
5 | | rusgranumwlk.l |
. . . 4
⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦
(#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) |
6 | 4, 5 | rusgranumwlklem4 26479 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃})) |
7 | 1, 2, 3, 6 | syl3an 1360 |
. 2
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃})) |
8 | | df-rab 2905 |
. . . . 5
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑤‘0) = 𝑃)} |
9 | | usgrav 25867 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
10 | 1, 9 | syl 17 |
. . . . . . . . . . . . 13
⊢
(〈𝑉, 𝐸〉 RegUSGrph 0 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
11 | 10, 3 | anim12i 588 |
. . . . . . . . . . . 12
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑁 ∈ ℕ) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈
ℕ0)) |
12 | 11 | 3adant2 1073 |
. . . . . . . . . . 11
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈
ℕ0)) |
13 | | df-3an 1033 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
↔ ((𝑉 ∈ V ∧
𝐸 ∈ V) ∧ 𝑁 ∈
ℕ0)) |
14 | 12, 13 | sylibr 223 |
. . . . . . . . . 10
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
15 | | iswwlkn 26212 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))) |
16 | | iswwlk 26211 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
17 | 16 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
18 | 17 | anbi1d 737 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))) |
19 | 15, 18 | bitrd 267 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))) |
20 | 14, 19 | syl 17 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))) |
21 | 20 | anbi1d 737 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑤‘0) = 𝑃) ↔ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ (𝑤‘0) = 𝑃))) |
22 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) =
(𝑁 + 1) →
((#‘𝑤) − 1) =
((𝑁 + 1) −
1)) |
23 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
24 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
25 | 23, 24 | pncand 10272 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
26 | 25 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑁 + 1) − 1) = 𝑁) |
27 | 22, 26 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . 16
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (#‘𝑤) = (𝑁 + 1)) → ((#‘𝑤) − 1) = 𝑁) |
28 | 27 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (#‘𝑤) = (𝑁 + 1)) → (0..^((#‘𝑤) − 1)) = (0..^𝑁)) |
29 | 28 | raleqdv 3121 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (#‘𝑤) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
30 | | rusgrargra 26457 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑉, 𝐸〉 RegUSGrph 0 →
〈𝑉, 𝐸〉 RegGrph 0) |
31 | | 0eusgraiff0rgra 26466 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 RegGrph 0 ↔ 𝐸 = ∅)) |
32 | | rneq 5272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐸 = ∅ → ran 𝐸 = ran ∅) |
33 | | rn0 5298 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ran
∅ = ∅ |
34 | 32, 33 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐸 = ∅ → ran 𝐸 = ∅) |
35 | 34 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐸 = ∅ → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ∅)) |
36 | | noel 3878 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ¬
{(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ∅ |
37 | 36 | bifal 1488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ∅ ↔
⊥) |
38 | 35, 37 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸 = ∅ → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥)) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥)) |
40 | 39 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁)⊥)) |
41 | | fal 1482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ¬
⊥ |
42 | 41 | ralf0 4030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑖 ∈
(0..^𝑁)⊥ ↔
(0..^𝑁) =
∅) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (∀𝑖 ∈ (0..^𝑁)⊥ ↔ (0..^𝑁) = ∅)) |
44 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℕ0 |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 0 ∈
ℕ0) |
46 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
47 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
48 | 45, 46, 47 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ ∧ 0 < 𝑁)) |
49 | 48 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ ∧ 0 < 𝑁)) |
50 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
(0..^𝑁) ↔ (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ ∧ 0 < 𝑁)) |
51 | 49, 50 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 0 ∈ (0..^𝑁)) |
52 | | fzon0 12356 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((0..^𝑁) ≠
∅ ↔ 0 ∈ (0..^𝑁)) |
53 | 51, 52 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (0..^𝑁) ≠ ∅) |
54 | 53 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ¬ (0..^𝑁) = ∅) |
55 | | nbfal 1486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(0..^𝑁) = ∅ ↔
((0..^𝑁) = ∅ ↔
⊥)) |
56 | 54, 55 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((0..^𝑁) = ∅ ↔
⊥)) |
57 | 40, 43, 56 | 3bitrd 293 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 = ∅ ∧ (𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥)) |
58 | 57 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 = ∅ → ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥))) |
59 | 31, 58 | syl6bi 242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 RegGrph 0 → ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥)))) |
60 | 1, 30, 59 | sylc 63 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑉, 𝐸〉 RegUSGrph 0 →
((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥))) |
61 | 60 | 3impib 1254 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥)) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (#‘𝑤) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥)) |
63 | 29, 62 | bitrd 267 |
. . . . . . . . . . . . 13
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (#‘𝑤) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ⊥)) |
64 | 63 | 3anbi3d 1397 |
. . . . . . . . . . . 12
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (#‘𝑤) = (𝑁 + 1)) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ⊥))) |
65 | | df-3an 1033 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ⊥) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉) ∧ ⊥)) |
66 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉) ∧ ⊥) ↔ (⊥ ∧ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉))) |
67 | 65, 66 | bitri 263 |
. . . . . . . . . . . 12
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ⊥) ↔ (⊥ ∧ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉))) |
68 | 64, 67 | syl6bb 275 |
. . . . . . . . . . 11
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (#‘𝑤) = (𝑁 + 1)) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (⊥ ∧ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉)))) |
69 | 68 | ex 449 |
. . . . . . . . . 10
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((#‘𝑤) = (𝑁 + 1) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (⊥ ∧ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉))))) |
70 | 69 | pm5.32rd 670 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ ((⊥ ∧ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉)) ∧ (#‘𝑤) = (𝑁 + 1)))) |
71 | 70 | anbi1d 737 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ (((⊥ ∧ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉)) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ (𝑤‘0) = 𝑃))) |
72 | | anass 679 |
. . . . . . . . . 10
⊢
((((⊥ ∧ (𝑤
≠ ∅ ∧ 𝑤 ∈
Word 𝑉)) ∧
(#‘𝑤) = (𝑁 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ ((⊥ ∧ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉)) ∧ ((#‘𝑤) = (𝑁 + 1) ∧ (𝑤‘0) = 𝑃))) |
73 | | anass 679 |
. . . . . . . . . . 11
⊢ (((⊥
∧ (𝑤 ≠ ∅ ∧
𝑤 ∈ Word 𝑉)) ∧ ((#‘𝑤) = (𝑁 + 1) ∧ (𝑤‘0) = 𝑃)) ↔ (⊥ ∧ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉) ∧ ((#‘𝑤) = (𝑁 + 1) ∧ (𝑤‘0) = 𝑃)))) |
74 | 41 | intnanr 952 |
. . . . . . . . . . . 12
⊢ ¬
(⊥ ∧ ((𝑤 ≠
∅ ∧ 𝑤 ∈ Word
𝑉) ∧ ((#‘𝑤) = (𝑁 + 1) ∧ (𝑤‘0) = 𝑃))) |
75 | 74 | bifal 1488 |
. . . . . . . . . . 11
⊢ ((⊥
∧ ((𝑤 ≠ ∅
∧ 𝑤 ∈ Word 𝑉) ∧ ((#‘𝑤) = (𝑁 + 1) ∧ (𝑤‘0) = 𝑃))) ↔ ⊥) |
76 | 73, 75 | bitri 263 |
. . . . . . . . . 10
⊢ (((⊥
∧ (𝑤 ≠ ∅ ∧
𝑤 ∈ Word 𝑉)) ∧ ((#‘𝑤) = (𝑁 + 1) ∧ (𝑤‘0) = 𝑃)) ↔ ⊥) |
77 | 72, 76 | bitri 263 |
. . . . . . . . 9
⊢
((((⊥ ∧ (𝑤
≠ ∅ ∧ 𝑤 ∈
Word 𝑉)) ∧
(#‘𝑤) = (𝑁 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ ⊥) |
78 | 77 | a1i 11 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((((⊥ ∧
(𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉)) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ ⊥)) |
79 | 21, 71, 78 | 3bitrd 293 |
. . . . . . 7
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑤‘0) = 𝑃) ↔ ⊥)) |
80 | 79 | abbidv 2728 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑤‘0) = 𝑃)} = {𝑤 ∣ ⊥}) |
81 | 41 | abf 3930 |
. . . . . 6
⊢ {𝑤 ∣ ⊥} =
∅ |
82 | 80, 81 | syl6eq 2660 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑤‘0) = 𝑃)} = ∅) |
83 | 8, 82 | syl5eq 2656 |
. . . 4
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} = ∅) |
84 | 83 | fveq2d 6107 |
. . 3
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (#‘∅)) |
85 | | hash0 13019 |
. . 3
⊢
(#‘∅) = 0 |
86 | 84, 85 | syl6eq 2660 |
. 2
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = 0) |
87 | 7, 86 | eqtrd 2644 |
1
⊢
((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑃𝐿𝑁) = 0) |