Metamath Proof Explorer

Theorem isewlk

Description: Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021)

		Ref	Expression
	Hypothesis	ewlksfval.i	$⊢ I = iEdg (G)$
	Assertion	isewlk	$⊢ (G \in W \land S \in ℕ_{0}^{*} \land F \in U) \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))\|))$

Proof

Step	Hyp	Ref	Expression
1		ewlksfval.i	$⊢ I = iEdg (G)$
2	1	ewlksfval	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to G EdgWalks S = \{f \| (f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|)\}$
3	2	3adant3	$⊢ (G \in W \land S \in ℕ_{0}^{*} \land F \in U) \to G EdgWalks S = \{f \| (f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|)\}$
4	3	eleq2d	$⊢ (G \in W \land S \in ℕ_{0}^{*} \land F \in U) \to (F \in (G EdgWalks S) \leftrightarrow F \in \{f \| (f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|)\})$
5		eleq1	$⊢ f = F \to (f \in Word dom I \leftrightarrow F \in Word dom I)$
6		fveq2	$⊢ f = F \to \|f\| = \|F\|$
7	6	oveq2d	$⊢ f = F \to (1 ..^\|f\|) = (1 ..^\|F\|)$
8		fveq1	$⊢ f = F \to f (k - 1) = F (k - 1)$
9	8	fveq2d	$⊢ f = F \to I (f (k - 1)) = I (F (k - 1))$
10		fveq1	$⊢ f = F \to f (k) = F (k)$
11	10	fveq2d	$⊢ f = F \to I (f (k)) = I (F (k))$
12	9 11	ineq12d	$⊢ f = F \to I (f (k - 1)) \cap I (f (k)) = I (F (k - 1)) \cap I (F (k))$
13	12	fveq2d	$⊢ f = F \to \|I (f (k - 1)) \cap I (f (k))\| = \|I (F (k - 1)) \cap I (F (k))\|$
14	13	breq2d	$⊢ f = F \to (S \leq \|I (f (k - 1)) \cap I (f (k))\| \leftrightarrow S \leq \|I (F (k - 1)) \cap I (F (k))\|)$
15	7 14	raleqbidv	$⊢ f = F \to (\forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\| \leftrightarrow \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|)$
16	5 15	anbi12d	$⊢ f = F \to ((f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|) \leftrightarrow (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
17	16	elabg	$⊢ F \in U \to (F \in \{f \| (f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|)\} \leftrightarrow (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
18	17	3ad2ant3	$⊢ (G \in W \land S \in ℕ_{0}^{*} \land F \in U) \to (F \in \{f \| (f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|)\} \leftrightarrow (F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|))$
19	4 18	bitrd	$⊢ (G \in W \land S \in ℕ_{0}^{*} \land F \in U) \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))\|))$