Metamath Proof Explorer


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