Metamath Proof Explorer

Theorem wwlksnextbij

Description: There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij.v ⊢V=Vtx⁡G
wwlksnextbij.e ⊢E=Edg⁡G
Assertion wwlksnextbij ⊢W∈NWWalksNG→∃ff:w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E

Proof

Step Hyp Ref Expression
1 wwlksnextbij.v ⊢V=Vtx⁡G
2 wwlksnextbij.e ⊢E=Edg⁡G
3 ovexd ⊢W∈NWWalksNG→N+1WWalksNG∈V
4 rabexg ⊢N+1WWalksNG∈V→t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E∈V
5 mptexg ⊢t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E∈V→x∈t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x∈V
6 3 4 5 3syl ⊢W∈NWWalksNG→x∈t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x∈V
7 eqid ⊢w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E=w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
8 preq2 ⊢n=p→lastS⁡Wn=lastS⁡Wp
9 8 eleq1d ⊢n=p→lastS⁡Wn∈E↔lastS⁡Wp∈E
10 9 cbvrabv ⊢n∈V|lastS⁡Wn∈E=p∈V|lastS⁡Wp∈E
11 fveqeq2 ⊢t=w→t=N+2↔w=N+2
12 oveq1 ⊢t=w→tprefixN+1=wprefixN+1
13 12 eqeq1d ⊢t=w→tprefixN+1=W↔wprefixN+1=W
14 fveq2 ⊢t=w→lastS⁡t=lastS⁡w
15 14 preq2d ⊢t=w→lastS⁡WlastS⁡t=lastS⁡WlastS⁡w
16 15 eleq1d ⊢t=w→lastS⁡WlastS⁡t∈E↔lastS⁡WlastS⁡w∈E
17 11 13 16 3anbi123d ⊢t=w→t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E↔w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
18 17 cbvrabv ⊢t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E=w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
19 18 mpteq1i ⊢x∈t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x=x∈w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟼lastS⁡x
20 1 2 7 10 19 wwlksnextbij0 ⊢W∈NWWalksNG→x∈t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x:w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E
21 eqid ⊢t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E=t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E
22 1 2 21 wwlksnextwrd ⊢W∈NWWalksNG→t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E=t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E
23 22 eqcomd ⊢W∈NWWalksNG→t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E=t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E
24 23 mpteq1d ⊢W∈NWWalksNG→x∈t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x=x∈t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x
25 1 2 7 wwlksnextwrd ⊢W∈NWWalksNG→w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E=w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E
26 25 eqcomd ⊢W∈NWWalksNG→w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E=w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
27 eqidd ⊢W∈NWWalksNG→n∈V|lastS⁡Wn∈E=n∈V|lastS⁡Wn∈E
28 24 26 27 f1oeq123d ⊢W∈NWWalksNG→x∈t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x:w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E↔x∈t∈WordV|t=N+2∧tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x:w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E
29 20 28 mpbird ⊢W∈NWWalksNG→x∈t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x:w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E
30 f1oeq1 ⊢f=x∈t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x→f:w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E↔x∈t∈N+1WWalksNG|tprefixN+1=W∧lastS⁡WlastS⁡t∈E⟼lastS⁡x:w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E
31 6 29 30 spcedv ⊢W∈NWWalksNG→∃ff:w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E⟶1-1 onton∈V|lastS⁡Wn∈E