Metamath Proof Explorer

Theorem wwlksn

Description: The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion wwlksn ⊢ N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ g = G → WWalks ⁡ g = WWalks ⁡ G
2 1 adantl ⊢ n = N ∧ g = G → WWalks ⁡ g = WWalks ⁡ G
3 oveq1 ⊢ n = N → n + 1 = N + 1
4 3 eqeq2d ⊢ n = N → w = n + 1 ↔ w = N + 1
5 4 adantr ⊢ n = N ∧ g = G → w = n + 1 ↔ w = N + 1
6 2 5 rabeqbidv ⊢ n = N ∧ g = G → w ∈ WWalks ⁡ g | w = n + 1 = w ∈ WWalks ⁡ G | w = N + 1
7 df-wwlksn ⊢ WWalksN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ WWalks ⁡ g | w = n + 1
8 fvex ⊢ WWalks ⁡ G ∈ V
9 8 rabex ⊢ w ∈ WWalks ⁡ G | w = N + 1 ∈ V
10 6 7 9 ovmpoa ⊢ N ∈ ℕ 0 ∧ G ∈ V → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
11 10 expcom ⊢ G ∈ V → N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
12 7 reldmmpo ⊢ Rel ⁡ dom ⁡ WWalksN
13 12 ovprc2 ⊢ ¬ G ∈ V → N WWalksN G = ∅
14 fvprc ⊢ ¬ G ∈ V → WWalks ⁡ G = ∅
15 14 rabeqdv ⊢ ¬ G ∈ V → w ∈ WWalks ⁡ G | w = N + 1 = w ∈ ∅ | w = N + 1
16 rab0 ⊢ w ∈ ∅ | w = N + 1 = ∅
17 15 16 eqtrdi ⊢ ¬ G ∈ V → w ∈ WWalks ⁡ G | w = N + 1 = ∅
18 13 17 eqtr4d ⊢ ¬ G ∈ V → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
19 18 a1d ⊢ ¬ G ∈ V → N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
20 11 19 pm2.61i ⊢ N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1