upgredginwlk

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

	Ref	Expression
Hypotheses	edginwlk.i	$⊢ I = iEdg (G)$
	edginwlk.e	$⊢ E = Edg (G)$
Assertion	upgredginwlk	$⊢ (G \in UPGraph \land F \in Word dom I) \to (K \in (0 ..^\|F\|) \to I (F (K)) \in E)$

Step	Hyp	Ref	Expression
1		edginwlk.i	$⊢ I = iEdg (G)$
2		edginwlk.e	$⊢ E = Edg (G)$
3		upgruhgr	$⊢ G \in UPGraph \to G \in UHGraph$
4	1	uhgrfun	$⊢ G \in UHGraph \to Fun I$
5	3 4	syl	$⊢ G \in UPGraph \to Fun I$
6	1 2	edginwlk	$⊢ (Fun I \land F \in Word dom I \land K \in (0 ..^\|F\|)) \to I (F (K)) \in E$
7	6	3expia	$⊢ (Fun I \land F \in Word dom I) \to (K \in (0 ..^\|F\|) \to I (F (K)) \in E)$
8	5 7	sylan	$⊢ (G \in UPGraph \land F \in Word dom I) \to (K \in (0 ..^\|F\|) \to I (F (K)) \in E)$

Metamath Proof Explorer