Step | Hyp | Ref
| Expression |
1 | | df-wwlkn 26208 |
. . 3
⊢ WWalksN
= (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)})) |
2 | | df-rab 2905 |
. . . . . . 7
⊢ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)} = {𝑤 ∣ (𝑤 ∈ (𝑣 WWalks 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))} |
3 | | iswwlk 26211 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) → (𝑤 ∈ (𝑣 WWalks 𝑒) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒))) |
4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 𝑛 ∈ ℕ0)
→ (𝑤 ∈ (𝑣 WWalks 𝑒) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒))) |
5 | 4 | anbi1d 737 |
. . . . . . . 8
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 𝑛 ∈ ℕ0)
→ ((𝑤 ∈ (𝑣 WWalks 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)))) |
6 | 5 | abbidv 2728 |
. . . . . . 7
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 𝑛 ∈ ℕ0)
→ {𝑤 ∣ (𝑤 ∈ (𝑣 WWalks 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))} = {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))}) |
7 | 2, 6 | syl5eq 2656 |
. . . . . 6
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 𝑛 ∈ ℕ0)
→ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)} = {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))}) |
8 | | 3anan12 1044 |
. . . . . . . . . 10
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ↔ (𝑤 ∈ Word 𝑣 ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒))) |
9 | 8 | anbi1i 727 |
. . . . . . . . 9
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)) ↔ ((𝑤 ∈ Word 𝑣 ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)) ∧ (#‘𝑤) = (𝑛 + 1))) |
10 | | anass 679 |
. . . . . . . . 9
⊢ (((𝑤 ∈ Word 𝑣 ∧ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)) ∧ (#‘𝑤) = (𝑛 + 1)) ↔ (𝑤 ∈ Word 𝑣 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)))) |
11 | 9, 10 | bitri 263 |
. . . . . . . 8
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)) ↔ (𝑤 ∈ Word 𝑣 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)))) |
12 | 11 | abbii 2726 |
. . . . . . 7
⊢ {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))} = {𝑤 ∣ (𝑤 ∈ Word 𝑣 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)))} |
13 | | df-rab 2905 |
. . . . . . 7
⊢ {𝑤 ∈ Word 𝑣 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))} = {𝑤 ∣ (𝑤 ∈ Word 𝑣 ∧ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1)))} |
14 | 12, 13 | eqtr4i 2635 |
. . . . . 6
⊢ {𝑤 ∣ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑣 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))} = {𝑤 ∈ Word 𝑣 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))} |
15 | 7, 14 | syl6eq 2660 |
. . . . 5
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 𝑛 ∈ ℕ0)
→ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)} = {𝑤 ∈ Word 𝑣 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))}) |
16 | 15 | mpteq2dva 4672 |
. . . 4
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) → (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)}) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ Word 𝑣 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))})) |
17 | 16 | mpt2eq3ia 6618 |
. . 3
⊢ (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)})) = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ Word 𝑣 ∣ ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))})) |
18 | 1, 17 | eqtri 2632 |
. 2
⊢ WWalksN
= (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ Word
𝑣 ∣ ((𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒) ∧ (#‘𝑤) = (𝑛 + 1))})) |
19 | 18 | elovmptnn0wrd 13203 |
1
⊢ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word 𝑉))) |