Metamath Proof Explorer

Theorem wspthsnon

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

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

Proof

Step Hyp Ref Expression
1 wwlksnon.v ⊢ V = Vtx ⁡ G
2 df-wspthsnon ⊢ WSPathsNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w
3 2 a1i ⊢ N ∈ ℕ 0 ∧ G ∈ U → WSPathsNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w
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 WWalksNOn g = N WWalksNOn G
8 7 oveqd ⊢ n = N ∧ g = G → a n WWalksNOn g b = a N WWalksNOn G b
9 fveq2 ⊢ g = G → SPathsOn ⁡ g = SPathsOn ⁡ G
10 9 oveqd ⊢ g = G → a SPathsOn ⁡ g b = a SPathsOn ⁡ G b
11 10 breqd ⊢ g = G → f a SPathsOn ⁡ g b w ↔ f a SPathsOn ⁡ G b w
12 11 adantl ⊢ n = N ∧ g = G → f a SPathsOn ⁡ g b w ↔ f a SPathsOn ⁡ G b w
13 12 exbidv ⊢ n = N ∧ g = G → ∃ f f a SPathsOn ⁡ g b w ↔ ∃ f f a SPathsOn ⁡ G b w
14 8 13 rabeqbidv ⊢ n = N ∧ g = G → w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w = w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w
15 6 6 14 mpoeq123dv ⊢ n = N ∧ g = G → a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w = a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w
16 15 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ U ∧ n = N ∧ g = G → a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w = a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w
17 simpl ⊢ N ∈ ℕ 0 ∧ G ∈ U → N ∈ ℕ 0
18 elex ⊢ G ∈ U → G ∈ V
19 18 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ U → G ∈ V
20 1 fvexi ⊢ V ∈ V
21 20 20 mpoex ⊢ a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w ∈ V
22 21 a1i ⊢ N ∈ ℕ 0 ∧ G ∈ U → a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w ∈ V
23 3 16 17 19 22 ovmpod ⊢ N ∈ ℕ 0 ∧ G ∈ U → N WSPathsNOn G = a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w