Step | Hyp | Ref
| Expression |
1 | | wwlkn 26210 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑉 WWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (𝑁 + 1)}) |
2 | | df-rab 2905 |
. . . . . . 7
⊢ {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (𝑁 + 1)} = {𝑤 ∣ (𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} |
3 | 2 | a1i 11 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (𝑁 + 1)} = {𝑤 ∣ (𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))}) |
4 | | iswwlk 26211 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
5 | 4 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
6 | 5 | anbi1d 737 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))) |
7 | 6 | abbidv 2728 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ {𝑤 ∣ (𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))}) |
8 | | 3anan12 1044 |
. . . . . . . . . . 11
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑤 ∈ Word 𝑉 ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
9 | 8 | anbi1i 727 |
. . . . . . . . . 10
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ ((𝑤 ∈ Word 𝑉 ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) ∧ (#‘𝑤) = (𝑁 + 1))) |
10 | | anass 679 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ Word 𝑉 ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))) |
11 | 9, 10 | bitri 263 |
. . . . . . . . 9
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))) |
12 | 11 | abbii 2726 |
. . . . . . . 8
⊢ {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))} |
13 | | df-rab 2905 |
. . . . . . . 8
⊢ {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)))} |
14 | 12, 13 | eqtr4i 2635 |
. . . . . . 7
⊢ {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} |
15 | 7, 14 | syl6eq 2660 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ {𝑤 ∣ (𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} = {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))}) |
16 | 1, 3, 15 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑉 WWalksN 𝐸)‘𝑁) = {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))}) |
17 | 16 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑉 ∈ Fin) →
((𝑉 WWalksN 𝐸)‘𝑁) = {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))}) |
18 | | peano2nn0 11210 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
19 | 18 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
ℕ0) |
20 | 19 | anim2i 591 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0))
→ (𝑉 ∈ Fin ∧
(𝑁 + 1) ∈
ℕ0)) |
21 | 20 | ancoms 468 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑉 ∈ Fin) →
(𝑉 ∈ Fin ∧ (𝑁 + 1) ∈
ℕ0)) |
22 | | wrdnfi 13193 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ (𝑁 + 1) ∈
ℕ0) → {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = (𝑁 + 1)} ∈ Fin) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑉 ∈ Fin) →
{𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = (𝑁 + 1)} ∈ Fin) |
24 | | simpr 476 |
. . . . . . 7
⊢ (((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) → (#‘𝑤) = (𝑁 + 1)) |
25 | 24 | rgenw 2908 |
. . . . . 6
⊢
∀𝑤 ∈
Word 𝑉(((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) → (#‘𝑤) = (𝑁 + 1)) |
26 | | ss2rab 3641 |
. . . . . 6
⊢ ({𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = (𝑁 + 1)} ↔ ∀𝑤 ∈ Word 𝑉(((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1)) → (#‘𝑤) = (𝑁 + 1))) |
27 | 25, 26 | mpbir 220 |
. . . . 5
⊢ {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = (𝑁 + 1)} |
28 | | ssfi 8065 |
. . . . 5
⊢ (({𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = (𝑁 + 1)} ∈ Fin ∧ {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} ⊆ {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = (𝑁 + 1)}) → {𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} ∈ Fin) |
29 | 23, 27, 28 | sylancl 693 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑉 ∈ Fin) →
{𝑤 ∈ Word 𝑉 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑤) = (𝑁 + 1))} ∈ Fin) |
30 | 17, 29 | eqeltrd 2688 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑉 ∈ Fin) →
((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin) |
31 | 30 | ex 449 |
. 2
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑉 ∈ Fin →
((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin)) |
32 | | wwlknndef 26265 |
. . . . 5
⊢ ((𝑉 ∉ V ∨ 𝐸 ∉ V ∨ 𝑁 ∉ ℕ0)
→ ((𝑉 WWalksN 𝐸)‘𝑁) = ∅) |
33 | | 3ioran 1049 |
. . . . . 6
⊢ (¬
(𝑉 ∉ V ∨ 𝐸 ∉ V ∨ 𝑁 ∉ ℕ0)
↔ (¬ 𝑉 ∉ V
∧ ¬ 𝐸 ∉ V
∧ ¬ 𝑁 ∉
ℕ0)) |
34 | | nnel 2892 |
. . . . . . 7
⊢ (¬
𝑉 ∉ V ↔ 𝑉 ∈ V) |
35 | | nnel 2892 |
. . . . . . 7
⊢ (¬
𝐸 ∉ V ↔ 𝐸 ∈ V) |
36 | | nnel 2892 |
. . . . . . 7
⊢ (¬
𝑁 ∉
ℕ0 ↔ 𝑁 ∈
ℕ0) |
37 | 34, 35, 36 | 3anbi123i 1244 |
. . . . . 6
⊢ ((¬
𝑉 ∉ V ∧ ¬
𝐸 ∉ V ∧ ¬
𝑁 ∉
ℕ0) ↔ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
38 | 33, 37 | sylbb 208 |
. . . . 5
⊢ (¬
(𝑉 ∉ V ∨ 𝐸 ∉ V ∨ 𝑁 ∉ ℕ0)
→ (𝑉 ∈ V ∧
𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
39 | 32, 38 | nsyl4 155 |
. . . 4
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑉 WWalksN 𝐸)‘𝑁) = ∅) |
40 | | 0fin 8073 |
. . . . 5
⊢ ∅
∈ Fin |
41 | 40 | a1i 11 |
. . . 4
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ∅ ∈ Fin) |
42 | 39, 41 | eqeltrd 2688 |
. . 3
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin) |
43 | 42 | a1d 25 |
. 2
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑉 ∈ Fin →
((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin)) |
44 | 31, 43 | pm2.61i 175 |
1
⊢ (𝑉 ∈ Fin → ((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin) |