Step | Hyp | Ref
| Expression |
1 | | wwlksn 26729 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) |
2 | | df-rab 2921 |
. . . . . . . 8
⊢ {𝑤 ∈ (WWalks‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} = {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1))} |
3 | 1, 2 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalksN 𝐺) = {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1))}) |
4 | 3 | adantl 482 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑁 WWalksN 𝐺) = {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1))}) |
5 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
7 | 5, 6 | iswwlks 26728 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (WWalks‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑤 ∈
(WWalks‘𝐺) ↔
(𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
9 | 8 | anbi1d 741 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑤 ∈
(WWalks‘𝐺) ∧
(#‘𝑤) = (𝑁 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)))) |
10 | 9 | abbidv 2741 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))}) |
11 | | 3anan12 1051 |
. . . . . . . . . . 11
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
12 | 11 | anbi1i 731 |
. . . . . . . . . 10
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (#‘𝑤) = (𝑁 + 1))) |
13 | | anass 681 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)))) |
14 | 12, 13 | bitri 264 |
. . . . . . . . 9
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)))) |
15 | 14 | abbii 2739 |
. . . . . . . 8
⊢ {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)))} |
16 | | df-rab 2921 |
. . . . . . . 8
⊢ {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)))} |
17 | 15, 16 | eqtr4i 2647 |
. . . . . . 7
⊢ {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} |
18 | 10, 17 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))}) |
19 | 4, 18 | eqtrd 2656 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑁 WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))}) |
20 | 19 | adantr 481 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (Vtx‘𝐺) ∈
Fin) → (𝑁 WWalksN
𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))}) |
21 | | peano2nn0 11333 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
22 | 21 | adantl 482 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
ℕ0) |
23 | 22 | anim2i 593 |
. . . . . . 7
⊢
(((Vtx‘𝐺)
∈ Fin ∧ (𝐺 ∈
V ∧ 𝑁 ∈
ℕ0)) → ((Vtx‘𝐺) ∈ Fin ∧ (𝑁 + 1) ∈
ℕ0)) |
24 | 23 | ancoms 469 |
. . . . . 6
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (Vtx‘𝐺) ∈
Fin) → ((Vtx‘𝐺)
∈ Fin ∧ (𝑁 + 1)
∈ ℕ0)) |
25 | | wrdnfi 13338 |
. . . . . 6
⊢
(((Vtx‘𝐺)
∈ Fin ∧ (𝑁 + 1)
∈ ℕ0) → {𝑤 ∈ Word (Vtx‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} ∈ Fin) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (Vtx‘𝐺) ∈
Fin) → {𝑤 ∈ Word
(Vtx‘𝐺) ∣
(#‘𝑤) = (𝑁 + 1)} ∈
Fin) |
27 | | simpr 477 |
. . . . . . 7
⊢ (((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)) → (#‘𝑤) = (𝑁 + 1)) |
28 | 27 | rgenw 2924 |
. . . . . 6
⊢
∀𝑤 ∈
Word (Vtx‘𝐺)(((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)) → (#‘𝑤) = (𝑁 + 1)) |
29 | | ss2rab 3678 |
. . . . . 6
⊢ ({𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} ↔ ∀𝑤 ∈ Word (Vtx‘𝐺)(((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1)) → (#‘𝑤) = (𝑁 + 1))) |
30 | 28, 29 | mpbir 221 |
. . . . 5
⊢ {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} |
31 | | ssfi 8180 |
. . . . 5
⊢ (({𝑤 ∈ Word (Vtx‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} ∈ Fin ∧ {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) → {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} ∈ Fin) |
32 | 26, 30, 31 | sylancl 694 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (Vtx‘𝐺) ∈
Fin) → {𝑤 ∈ Word
(Vtx‘𝐺) ∣
((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑤) = (𝑁 + 1))} ∈ Fin) |
33 | 20, 32 | eqeltrd 2701 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (Vtx‘𝐺) ∈
Fin) → (𝑁 WWalksN
𝐺) ∈
Fin) |
34 | 33 | ex 450 |
. 2
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((Vtx‘𝐺)
∈ Fin → (𝑁
WWalksN 𝐺) ∈
Fin)) |
35 | | wwlksnndef 26800 |
. . . . 5
⊢ ((𝐺 ∉ V ∨ 𝑁 ∉ ℕ0)
→ (𝑁 WWalksN 𝐺) = ∅) |
36 | | ioran 511 |
. . . . . 6
⊢ (¬
(𝐺 ∉ V ∨ 𝑁 ∉ ℕ0)
↔ (¬ 𝐺 ∉ V
∧ ¬ 𝑁 ∉
ℕ0)) |
37 | | nnel 2906 |
. . . . . . 7
⊢ (¬
𝐺 ∉ V ↔ 𝐺 ∈ V) |
38 | | nnel 2906 |
. . . . . . 7
⊢ (¬
𝑁 ∉
ℕ0 ↔ 𝑁 ∈
ℕ0) |
39 | 37, 38 | anbi12i 733 |
. . . . . 6
⊢ ((¬
𝐺 ∉ V ∧ ¬
𝑁 ∉
ℕ0) ↔ (𝐺 ∈ V ∧ 𝑁 ∈
ℕ0)) |
40 | 36, 39 | sylbb 209 |
. . . . 5
⊢ (¬
(𝐺 ∉ V ∨ 𝑁 ∉ ℕ0)
→ (𝐺 ∈ V ∧
𝑁 ∈
ℕ0)) |
41 | 35, 40 | nsyl4 156 |
. . . 4
⊢ (¬
(𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑁 WWalksN 𝐺) = ∅) |
42 | | 0fin 8188 |
. . . . 5
⊢ ∅
∈ Fin |
43 | 42 | a1i 11 |
. . . 4
⊢ (¬
(𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ∅ ∈ Fin) |
44 | 41, 43 | eqeltrd 2701 |
. . 3
⊢ (¬
(𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑁 WWalksN 𝐺) ∈ Fin) |
45 | 44 | a1d 25 |
. 2
⊢ (¬
(𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((Vtx‘𝐺)
∈ Fin → (𝑁
WWalksN 𝐺) ∈
Fin)) |
46 | 34, 45 | pm2.61i 176 |
1
⊢
((Vtx‘𝐺)
∈ Fin → (𝑁
WWalksN 𝐺) ∈
Fin) |