Metamath Proof Explorer

Theorem wwlksnon

Description: The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 11-May-2021)

Ref Expression
Hypothesis wwlksnon.v ⊢ V = Vtx ⁡ G
Assertion wwlksnon ⊢ N ∈ ℕ 0 ∧ G ∈ U → N WWalksNOn G = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b

Proof

Step Hyp Ref Expression
1 wwlksnon.v ⊢ V = Vtx ⁡ G
2 df-wwlksnon ⊢ WWalksNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b
3 2 a1i ⊢ N ∈ ℕ 0 ∧ G ∈ U → WWalksNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b
4 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
5 4 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
6 5 adantl ⊢ n = N ∧ g = G → Vtx ⁡ g = V
7 oveq12 ⊢ n = N ∧ g = G → n WWalksN g = N WWalksN G
8 fveqeq2 ⊢ n = N → w ⁡ n = b ↔ w ⁡ N = b
9 8 anbi2d ⊢ n = N → w ⁡ 0 = a ∧ w ⁡ n = b ↔ w ⁡ 0 = a ∧ w ⁡ N = b
10 9 adantr ⊢ n = N ∧ g = G → w ⁡ 0 = a ∧ w ⁡ n = b ↔ w ⁡ 0 = a ∧ w ⁡ N = b
11 7 10 rabeqbidv ⊢ n = N ∧ g = G → w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b = w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b
12 6 6 11 mpoeq123dv ⊢ n = N ∧ g = G → a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b
13 12 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ U ∧ n = N ∧ g = G → a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b
14 simpl ⊢ N ∈ ℕ 0 ∧ G ∈ U → N ∈ ℕ 0
15 elex ⊢ G ∈ U → G ∈ V
16 15 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ U → G ∈ V
17 1 fvexi ⊢ V ∈ V
18 17 17 mpoex ⊢ a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b ∈ V
19 18 a1i ⊢ N ∈ ℕ 0 ∧ G ∈ U → a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b ∈ V
20 3 13 14 16 19 ovmpod ⊢ N ∈ ℕ 0 ∧ G ∈ U → N WWalksNOn G = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b