Metamath Proof Explorer

Theorem edginwlk

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) (Revised by AV, 9-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		edginwlk.i	$⊢ I = iEdg (G)$
2		edginwlk.e	$⊢ E = Edg (G)$
3		simp1	$⊢ (Fun I \land F \in Word dom I \land K \in (0 ..^\|F\|)) \to Fun I$
4		wrdsymbcl	$⊢ (F \in Word dom I \land K \in (0 ..^\|F\|)) \to F (K) \in dom I$
5	4	3adant1	$⊢ (Fun I \land F \in Word dom I \land K \in (0 ..^\|F\|)) \to F (K) \in dom I$
6		fvelrn	$⊢ (Fun I \land F (K) \in dom I) \to I (F (K)) \in ran I$
7	3 5 6	syl2anc	$⊢ (Fun I \land F \in Word dom I \land K \in (0 ..^\|F\|)) \to I (F (K)) \in ran I$
8		edgval	$⊢ Edg (G) = ran iEdg (G)$
9	1	eqcomi	$⊢ iEdg (G) = I$
10	9	rneqi	$⊢ ran iEdg (G) = ran I$
11	2 8 10	3eqtri	$⊢ E = ran I$
12	7 11	eleqtrrdi	$⊢ (Fun I \land F \in Word dom I \land K \in (0 ..^\|F\|)) \to I (F (K)) \in E$