Metamath Proof Explorer

Theorem ewlkprop

Description: Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021)

		Ref	Expression
	Hypothesis	ewlksfval.i	$⊢ I = iEdg (G)$
	Assertion	ewlkprop	$⊢ F \in (G EdgWalks S) \to ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|)$

Proof

Step	Hyp	Ref	Expression
1		ewlksfval.i	$⊢ I = iEdg (G)$
2		df-ewlks	$⊢ EdgWalks = (g \in V, s \in ℕ_{0}^{*} ⟼ \{f \| \underset{˙}{[} iEdg (g) / i \underset{˙}{]} (f \in Word dom i \land \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|)\})$
3	2	elmpocl	$⊢ F \in (G EdgWalks S) \to (G \in V \land S \in ℕ_{0}^{*})$
4		simpr	$⊢ (F \in (G EdgWalks S) \land (G \in V \land S \in ℕ_{0}^{})) \to (G \in V \land S \in ℕ_{0}^{})$
5	1	isewlk	$⊢ (G \in V \land S \in ℕ_{0}^{*} \land F \in (G EdgWalks S)) \to (F \in (G EdgWalks S) \leftrightarrow (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
6	5	3expa	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in (G EdgWalks S)) \to (F \in (G EdgWalks S) \leftrightarrow (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
7	6	biimpd	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in (G EdgWalks S)) \to (F \in (G EdgWalks S) \to (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
8	7	expcom	$⊢ F \in (G EdgWalks S) \to ((G \in V \land S \in ℕ_{0}^{*}) \to (F \in (G EdgWalks S) \to (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|)))$
9	8	pm2.43a	$⊢ F \in (G EdgWalks S) \to ((G \in V \land S \in ℕ_{0}^{*}) \to (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
10	9	imp	$⊢ (F \in (G EdgWalks S) \land (G \in V \land S \in ℕ_{0}^{*})) \to (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|)$
11		3anass	$⊢ ((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|) \leftrightarrow ((G \in V \land S \in ℕ_{0}^{}) \land (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
12	4 10 11	sylanbrc	$⊢ (F \in (G EdgWalks S) \land (G \in V \land S \in ℕ_{0}^{})) \to ((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|)$
13	3 12	mpdan	$⊢ F \in (G EdgWalks S) \to ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|)$