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