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

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