iedginwlk

Description: The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 23-Apr-2021)

		Ref	Expression
	Hypothesis	iedginwlk.i	$⊢ I = iEdg (G)$
	Assertion	iedginwlk	$⊢ (Fun I \land F Walks (G) P \land X \in (0 ..^\|F\|)) \to I (F (X)) \in ran I$

Step	Hyp	Ref	Expression
1		iedginwlk.i	$⊢ I = iEdg (G)$
2		simp1	$⊢ (Fun I \land F Walks (G) P \land X \in (0 ..^\|F\|)) \to Fun I$
3	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
4	3	3ad2ant2	$⊢ (Fun I \land F Walks (G) P \land X \in (0 ..^\|F\|)) \to F \in Word dom I$
5		simp3	$⊢ (Fun I \land F Walks (G) P \land X \in (0 ..^\|F\|)) \to X \in (0 ..^\|F\|)$
6		wrdsymbcl	$⊢ (F \in Word dom I \land X \in (0 ..^\|F\|)) \to F (X) \in dom I$
7	4 5 6	syl2anc	$⊢ (Fun I \land F Walks (G) P \land X \in (0 ..^\|F\|)) \to F (X) \in dom I$
8		fvelrn	$⊢ (Fun I \land F (X) \in dom I) \to I (F (X)) \in ran I$
9	2 7 8	syl2anc	$⊢ (Fun I \land F Walks (G) P \land X \in (0 ..^\|F\|)) \to I (F (X)) \in ran I$

Metamath Proof Explorer