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 ∈ 0 ..^ F → P ⁡ N P ⁡ N + 1 ⊆ 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 → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ 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 ⊆ I ⁡ F ⁡ k ↔ P ⁡ N P ⁡ N + 1 ⊆ I ⁡ F ⁡ N
10 9 rspccv ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → N ∈ 0 ..^ F → P ⁡ N P ⁡ N + 1 ⊆ I ⁡ F ⁡ N
11 3 4 10 3syl ⊢ F EulerPaths ⁡ G P → N ∈ 0 ..^ F → P ⁡ N P ⁡ N + 1 ⊆ I ⁡ F ⁡ N
12 11 imp ⊢ F EulerPaths ⁡ G P ∧ N ∈ 0 ..^ F → P ⁡ N P ⁡ N + 1 ⊆ I ⁡ F ⁡ N