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=iEdgG
Assertion upgreupthseg GUPGraphFEulerPathsGPN0..^FIFN=PNPN+1

Proof

Step Hyp Ref Expression
1 upgreupthseg.i I=iEdgG
2 eqid VtxG=VtxG
3 1 2 upgreupthi GUPGraphFEulerPathsGPF:0..^F1-1 ontodomIP:0FVtxGn0..^FIFn=PnPn+1
4 2fveq3 n=NIFn=IFN
5 fveq2 n=NPn=PN
6 fvoveq1 n=NPn+1=PN+1
7 5 6 preq12d n=NPnPn+1=PNPN+1
8 4 7 eqeq12d n=NIFn=PnPn+1IFN=PNPN+1
9 8 rspccv n0..^FIFn=PnPn+1N0..^FIFN=PNPN+1
10 9 3ad2ant3 F:0..^F1-1 ontodomIP:0FVtxGn0..^FIFn=PnPn+1N0..^FIFN=PNPN+1
11 3 10 syl GUPGraphFEulerPathsGPN0..^FIFN=PNPN+1
12 11 3impia GUPGraphFEulerPathsGPN0..^FIFN=PNPN+1