Metamath Proof Explorer


Theorem upgreupthseg

Description: The N -th edge in an eulerian path is the edge from P ( N ) to P ( N + 1 ) . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

Ref Expression
Hypothesis upgreupthseg.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion upgreupthseg ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑁 ) ) = { ( 𝑃𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )

Proof

Step Hyp Ref Expression
1 upgreupthseg.i 𝐼 = ( iEdg ‘ 𝐺 )
2 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 1 2 upgreupthi ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑛 ) ) = { ( 𝑃𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) )
4 2fveq3 ( 𝑛 = 𝑁 → ( 𝐼 ‘ ( 𝐹𝑛 ) ) = ( 𝐼 ‘ ( 𝐹𝑁 ) ) )
5 fveq2 ( 𝑛 = 𝑁 → ( 𝑃𝑛 ) = ( 𝑃𝑁 ) )
6 fvoveq1 ( 𝑛 = 𝑁 → ( 𝑃 ‘ ( 𝑛 + 1 ) ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
7 5 6 preq12d ( 𝑛 = 𝑁 → { ( 𝑃𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } = { ( 𝑃𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
8 4 7 eqeq12d ( 𝑛 = 𝑁 → ( ( 𝐼 ‘ ( 𝐹𝑛 ) ) = { ( 𝑃𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹𝑁 ) ) = { ( 𝑃𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) )
9 8 rspccv ( ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑛 ) ) = { ( 𝑃𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹𝑁 ) ) = { ( 𝑃𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) )
10 9 3ad2ant3 ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑛 ) ) = { ( 𝑃𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹𝑁 ) ) = { ( 𝑃𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) )
11 3 10 syl ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹𝑁 ) ) = { ( 𝑃𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) )
12 11 3impia ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑁 ) ) = { ( 𝑃𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )