Theorem eupthseg

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

	Ref	Expression
Hypothesis	eupths.i	|- I = ( iEdg ` G )
Assertion	eupthseg	|- ( ( F ( EulerPaths ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		eupths.i	|- I = ( iEdg ` G )
2	1	eupthi	|- ( F ( EulerPaths ` G ) P -> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) )
3	2	simpld	|- ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
4	1	wlkvtxeledg	|- ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
5		fveq2	|- ( k = N -> ( P ` k ) = ( P ` N ) )
6		fvoveq1	|- ( k = N -> ( P ` ( k + 1 ) ) = ( P ` ( N + 1 ) ) )
7	5 6	preq12d	|- ( k = N -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
8		2fveq3	|- ( k = N -> ( I ` ( F ` k ) ) = ( I ` ( F ` N ) ) )
9	7 8	sseq12d	|- ( k = N -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
10	9	rspccv	|- ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> ( N e. ( 0 ..^ ( # ` F ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
11	3 4 10	3syl	|- ( F ( EulerPaths ` G ) P -> ( N e. ( 0 ..^ ( # ` F ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
12	11	imp	|- ( ( F ( EulerPaths ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) )