wlkprop

	Ref	Expression
Hypotheses	wksfval.v	$⊢ V = Vtx (G)$
	wksfval.i	$⊢ I = iEdg (G)$
Assertion	wlkprop	$⊢ F Walks (G) P \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$

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

Metamath Proof Explorer