Step | Hyp | Ref
| Expression |
1 | | wrdnfi 13989 |
. . . 4
⊢
((Vtx‘𝐺)
∈ Fin → {𝑤 ∈
Word (Vtx‘𝐺) ∣
(♯‘𝑤) = (𝑁 + 1)} ∈
Fin) |
2 | | simpr 488 |
. . . . . . 7
⊢ (((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)) → (♯‘𝑤) = (𝑁 + 1)) |
3 | 2 | rgenw 3065 |
. . . . . 6
⊢
∀𝑤 ∈
Word (Vtx‘𝐺)(((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)) → (♯‘𝑤) = (𝑁 + 1)) |
4 | | ss2rab 3960 |
. . . . . 6
⊢ ({𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)} ↔ ∀𝑤 ∈ Word (Vtx‘𝐺)(((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)) → (♯‘𝑤) = (𝑁 + 1))) |
5 | 3, 4 | mpbir 234 |
. . . . 5
⊢ {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)} |
6 | 5 | a1i 11 |
. . . 4
⊢
((Vtx‘𝐺)
∈ Fin → {𝑤 ∈
Word (Vtx‘𝐺) ∣
((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) |
7 | 1, 6 | ssfid 8819 |
. . 3
⊢
((Vtx‘𝐺)
∈ Fin → {𝑤 ∈
Word (Vtx‘𝐺) ∣
((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} ∈ Fin) |
8 | | wwlksn 27775 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) |
9 | | df-rab 3062 |
. . . . . 6
⊢ {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)} = {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (𝑁 + 1))} |
10 | 8, 9 | eqtrdi 2789 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalksN 𝐺) = {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (𝑁 + 1))}) |
11 | | 3anan12 1097 |
. . . . . . . . 9
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
12 | 11 | anbi1i 627 |
. . . . . . . 8
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)) ↔ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (♯‘𝑤) = (𝑁 + 1))) |
13 | | anass 472 |
. . . . . . . 8
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (♯‘𝑤) = (𝑁 + 1)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)))) |
14 | 12, 13 | bitri 278 |
. . . . . . 7
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)))) |
15 | 14 | abbii 2803 |
. . . . . 6
⊢ {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)))} |
16 | | eqid 2738 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
17 | | eqid 2738 |
. . . . . . . . 9
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
18 | 16, 17 | iswwlks 27774 |
. . . . . . . 8
⊢ (𝑤 ∈ (WWalks‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
19 | 18 | anbi1i 627 |
. . . . . . 7
⊢ ((𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (𝑁 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))) |
20 | 19 | abbii 2803 |
. . . . . 6
⊢ {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} |
21 | | df-rab 3062 |
. . . . . 6
⊢ {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ (𝑤 ∈ Word (Vtx‘𝐺) ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1)))} |
22 | 15, 20, 21 | 3eqtr4i 2771 |
. . . . 5
⊢ {𝑤 ∣ (𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (𝑁 + 1))} = {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} |
23 | 10, 22 | eqtrdi 2789 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))}) |
24 | 23 | eleq1d 2817 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 WWalksN 𝐺) ∈ Fin ↔ {𝑤 ∈ Word (Vtx‘𝐺) ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (𝑁 + 1))} ∈ Fin)) |
25 | 7, 24 | syl5ibr 249 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((Vtx‘𝐺)
∈ Fin → (𝑁
WWalksN 𝐺) ∈
Fin)) |
26 | | df-nel 3039 |
. . . . . . 7
⊢ (𝑁 ∉ ℕ0
↔ ¬ 𝑁 ∈
ℕ0) |
27 | 26 | biimpri 231 |
. . . . . 6
⊢ (¬
𝑁 ∈
ℕ0 → 𝑁 ∉
ℕ0) |
28 | 27 | olcd 873 |
. . . . 5
⊢ (¬
𝑁 ∈
ℕ0 → (𝐺 ∉ V ∨ 𝑁 ∉
ℕ0)) |
29 | | wwlksnndef 27843 |
. . . . 5
⊢ ((𝐺 ∉ V ∨ 𝑁 ∉ ℕ0)
→ (𝑁 WWalksN 𝐺) = ∅) |
30 | 28, 29 | syl 17 |
. . . 4
⊢ (¬
𝑁 ∈
ℕ0 → (𝑁 WWalksN 𝐺) = ∅) |
31 | | 0fin 8770 |
. . . 4
⊢ ∅
∈ Fin |
32 | 30, 31 | eqeltrdi 2841 |
. . 3
⊢ (¬
𝑁 ∈
ℕ0 → (𝑁 WWalksN 𝐺) ∈ Fin) |
33 | 32 | a1d 25 |
. 2
⊢ (¬
𝑁 ∈
ℕ0 → ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)) |
34 | 25, 33 | pm2.61i 185 |
1
⊢
((Vtx‘𝐺)
∈ Fin → (𝑁
WWalksN 𝐺) ∈
Fin) |