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 
|- I = ( iEdg ` G )
Assertion upgreupthseg 
|- ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )

Proof

Step Hyp Ref Expression
1 upgreupthseg.i 
 |-  I = ( iEdg ` G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 1 2 upgreupthi 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. n e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` n ) ) = { ( P ` n ) , ( P ` ( n + 1 ) ) } ) )
4 2fveq3 
 |-  ( n = N -> ( I ` ( F ` n ) ) = ( I ` ( F ` N ) ) )
5 fveq2 
 |-  ( n = N -> ( P ` n ) = ( P ` N ) )
6 fvoveq1 
 |-  ( n = N -> ( P ` ( n + 1 ) ) = ( P ` ( N + 1 ) ) )
7 5 6 preq12d 
 |-  ( n = N -> { ( P ` n ) , ( P ` ( n + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
8 4 7 eqeq12d 
 |-  ( n = N -> ( ( I ` ( F ` n ) ) = { ( P ` n ) , ( P ` ( n + 1 ) ) } <-> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) )
9 8 rspccv 
 |-  ( A. n e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` n ) ) = { ( P ` n ) , ( P ` ( n + 1 ) ) } -> ( N e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) )
10 9 3ad2ant3 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. n e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` n ) ) = { ( P ` n ) , ( P ` ( n + 1 ) ) } ) -> ( N e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) )
11 3 10 syl 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( N e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) )
12 11 3impia 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )