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→∃ff:p∈Walks⁡G|1st⁡p=N∧2nd⁡p⁡0=X⟶1-1 ontow∈NWWalksNG|w⁡0=X

Proof

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