Metamath Proof Explorer

Theorem wspthsn

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

Ref Expression
Assertion wspthsn ⊢ N WSPathsN G = w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w

Proof

Step Hyp Ref Expression
1 oveq12 ⊢ n = N ∧ g = G → n WWalksN g = N WWalksN G
2 fveq2 ⊢ g = G → SPaths ⁡ g = SPaths ⁡ G
3 2 breqd ⊢ g = G → f SPaths ⁡ g w ↔ f SPaths ⁡ G w
4 3 exbidv ⊢ g = G → ∃ f f SPaths ⁡ g w ↔ ∃ f f SPaths ⁡ G w
5 4 adantl ⊢ n = N ∧ g = G → ∃ f f SPaths ⁡ g w ↔ ∃ f f SPaths ⁡ G w
6 1 5 rabeqbidv ⊢ n = N ∧ g = G → w ∈ n WWalksN g | ∃ f f SPaths ⁡ g w = w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w
7 df-wspthsn ⊢ WSPathsN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ n WWalksN g | ∃ f f SPaths ⁡ g w
8 ovex ⊢ N WWalksN G ∈ V
9 8 rabex ⊢ w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w ∈ V
10 6 7 9 ovmpoa ⊢ N ∈ ℕ 0 ∧ G ∈ V → N WSPathsN G = w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w
11 7 mpondm0 ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N WSPathsN G = ∅
12 df-wwlksn ⊢ WWalksN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ WWalks ⁡ g | w = n + 1
13 12 mpondm0 ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N WWalksN G = ∅
14 13 rabeqdv ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w = w ∈ ∅ | ∃ f f SPaths ⁡ G w
15 rab0 ⊢ w ∈ ∅ | ∃ f f SPaths ⁡ G w = ∅
16 14 15 eqtrdi ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w = ∅
17 11 16 eqtr4d ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N WSPathsN G = w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w
18 10 17 pm2.61i ⊢ N WSPathsN G = w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w