This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) } )