Metamath Proof Explorer

Theorem wlknwwlksnen

Description: In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 5-Aug-2022)

Ref Expression
Assertion wlknwwlksnen ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G | 1 st ⁡ p = N ≈ N WWalksN G

Proof

Step Hyp Ref Expression
1 eqid ⊢ p ∈ Walks ⁡ G | 1 st ⁡ p = N = p ∈ Walks ⁡ G | 1 st ⁡ p = N
2 eqid ⊢ N WWalksN G = N WWalksN G
3 eqid ⊢ w ∈ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟼ 2 nd ⁡ w = w ∈ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟼ 2 nd ⁡ w
4 1 2 3 wlknwwlksnbij ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → w ∈ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟼ 2 nd ⁡ w : p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟶ 1-1 onto N WWalksN G
5 fvex ⊢ Walks ⁡ G ∈ V
6 5 rabex ⊢ p ∈ Walks ⁡ G | 1 st ⁡ p = N ∈ V
7 6 f1oen ⊢ w ∈ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟼ 2 nd ⁡ w : p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟶ 1-1 onto N WWalksN G → p ∈ Walks ⁡ G | 1 st ⁡ p = N ≈ N WWalksN G
8 4 7 syl ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G | 1 st ⁡ p = N ≈ N WWalksN G