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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wwlksnextbij.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion wwlksnextbij ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } )

Proof

Step Hyp Ref Expression
1 wwlksnextbij.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlksnextbij.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 ovexd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∈ V )
4 rabexg ⊢ ( ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∈ V → { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ∈ V )
5 mptexg ⊢ ( { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ∈ V → ( 𝑥 ∈ { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) ∈ V )
6 3 4 5 3syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑥 ∈ { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) ∈ V )
7 eqid ⊢ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
8 preq2 ⊢ ( 𝑛 = 𝑝 → { ( lastS ‘ 𝑊 ) , 𝑛 } = { ( lastS ‘ 𝑊 ) , 𝑝 } )
9 8 eleq1d ⊢ ( 𝑛 = 𝑝 → ( { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , 𝑝 } ∈ 𝐸 ) )
10 9 cbvrabv ⊢ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } = { 𝑝 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑝 } ∈ 𝐸 }
11 fveqeq2 ⊢ ( 𝑡 = 𝑤 → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ↔ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) )
12 oveq1 ⊢ ( 𝑡 = 𝑤 → ( 𝑡 prefix ( 𝑁 + 1 ) ) = ( 𝑤 prefix ( 𝑁 + 1 ) ) )
13 12 eqeq1d ⊢ ( 𝑡 = 𝑤 → ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
14 fveq2 ⊢ ( 𝑡 = 𝑤 → ( lastS ‘ 𝑡 ) = ( lastS ‘ 𝑤 ) )
15 14 preq2d ⊢ ( 𝑡 = 𝑤 → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } )
16 15 eleq1d ⊢ ( 𝑡 = 𝑤 → ( { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) )
17 11 13 16 3anbi123d ⊢ ( 𝑡 = 𝑤 → ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ↔ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) )
18 17 cbvrabv ⊢ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
19 18 mpteq1i ⊢ ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) )
20 1 2 7 10 19 wwlksnextbij0 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } )
21 eqid ⊢ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } = { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) }
22 1 2 21 wwlksnextwrd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } = { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } )
23 22 eqcomd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } = { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } )
24 23 mpteq1d ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑥 ∈ { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) )
25 1 2 7 wwlksnextwrd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } )
26 25 eqcomd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } )
27 eqidd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } )
28 24 26 27 f1oeq123d ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑥 ∈ { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } ↔ ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } ) )
29 20 28 mpbird ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑥 ∈ { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } )
30 f1oeq1 ⊢ ( 𝑓 = ( 𝑥 ∈ { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) → ( 𝑓 : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } ↔ ( 𝑥 ∈ { 𝑡 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) } ↦ ( lastS ‘ 𝑥 ) ) : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } ) )
31 6 29 30 spcedv ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } )