wlkv

Description: The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 3-Feb-2021)

		Ref	Expression
	Assertion	wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3	1 2	wksfval	$⊢ G \in V \to Walks (G) = \{⟨f, p⟩ \| (f \in Word dom iEdg (G) \land p : (0 \dots \|f\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (G) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (G) (f (k))))\}$
4	3	brfvopab	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$

Metamath Proof Explorer