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 \land N \in (0 ..^\|F\|)) \to \{P (N), P (N + 1)\} \subseteq I (F (N))$

Proof

Step	Hyp	Ref	Expression
1		eupths.i	$⊢ I = iEdg (G)$
2	1	eupthi	$⊢ F EulerPaths (G) P \to (F Walks (G) P \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I)$
3	2	simpld	$⊢ F EulerPaths (G) P \to F Walks (G) P$
4	1	wlkvtxeledg	$⊢ F Walks (G) P \to \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \subseteq I (F (k))$
5		fveq2	$⊢ k = N \to P (k) = P (N)$
6		fvoveq1	$⊢ k = N \to P (k + 1) = P (N + 1)$
7	5 6	preq12d	$⊢ k = N \to \{P (k), P (k + 1)\} = \{P (N), P (N + 1)\}$
8		2fveq3	$⊢ k = N \to I (F (k)) = I (F (N))$
9	7 8	sseq12d	$⊢ k = N \to (\{P (k), P (k + 1)\} \subseteq I (F (k)) \leftrightarrow \{P (N), P (N + 1)\} \subseteq I (F (N)))$
10	9	rspccv	$⊢ \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \subseteq I (F (k)) \to (N \in (0 ..^\|F\|) \to \{P (N), P (N + 1)\} \subseteq I (F (N)))$
11	3 4 10	3syl	$⊢ F EulerPaths (G) P \to (N \in (0 ..^\|F\|) \to \{P (N), P (N + 1)\} \subseteq I (F (N)))$
12	11	imp	$⊢ (F EulerPaths (G) P \land N \in (0 ..^\|F\|)) \to \{P (N), P (N + 1)\} \subseteq I (F (N))$