Metamath Proof Explorer

Theorem wlksnwwlknvbij

Description: There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 5-Aug-2022)

Ref Expression
Assertion wlksnwwlknvbij ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → ∃ f f : p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X

Proof

Step Hyp Ref Expression
1 fvex ⊢ Walks ⁡ G ∈ V
2 1 mptrabex ⊢ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p ∈ V
3 2 resex ⊢ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p ↾ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ∈ V
4 eqid ⊢ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p = p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p
5 eqid ⊢ q ∈ Walks ⁡ G | 1 st ⁡ q = N = q ∈ Walks ⁡ G | 1 st ⁡ q = N
6 eqid ⊢ N WWalksN G = N WWalksN G
7 5 6 4 wlknwwlksnbij ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p : q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟶ 1-1 onto N WWalksN G
8 fveq1 ⊢ w = 2 nd ⁡ p → w ⁡ 0 = 2 nd ⁡ p ⁡ 0
9 8 eqeq1d ⊢ w = 2 nd ⁡ p → w ⁡ 0 = X ↔ 2 nd ⁡ p ⁡ 0 = X
10 9 3ad2ant3 ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ∧ w = 2 nd ⁡ p → w ⁡ 0 = X ↔ 2 nd ⁡ p ⁡ 0 = X
11 4 7 10 f1oresrab ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p ↾ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X
12 f1oeq1 ⊢ f = p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p ↾ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X → f : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X ↔ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p ↾ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X
13 12 spcegv ⊢ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p ↾ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ∈ V → p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N ⟼ 2 nd ⁡ p ↾ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X → ∃ f f : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X
14 3 11 13 mpsyl ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → ∃ f f : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X
15 2fveq3 ⊢ p = q → 1 st ⁡ p = 1 st ⁡ q
16 15 eqeq1d ⊢ p = q → 1 st ⁡ p = N ↔ 1 st ⁡ q = N
17 16 rabrabi ⊢ p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X = p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X
18 17 eqcomi ⊢ p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X = p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X
19 f1oeq2 ⊢ p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X = p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X → f : p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X ↔ f : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X
20 18 19 mp1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → f : p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X ↔ f : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X
21 20 exbidv ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → ∃ f f : p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X ↔ ∃ f f : p ∈ q ∈ Walks ⁡ G | 1 st ⁡ q = N | 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X
22 14 21 mpbird ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → ∃ f f : p ∈ Walks ⁡ G | 1 st ⁡ p = N ∧ 2 nd ⁡ p ⁡ 0 = X ⟶ 1-1 onto w ∈ N WWalksN G | w ⁡ 0 = X