ewlksfval

Description: The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021)

		Ref	Expression
	Hypothesis	ewlksfval.i	$⊢ I = iEdg (G)$
	Assertion	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))\|)\}$

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	a1i	$⊢ (G \in W \land S \in ℕ_{0}^{}) \to 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))\|)\})$
4		fvexd	$⊢ (g = G \land s = S) \to iEdg (g) \in V$
5		simpr	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to i = iEdg (g)$
6		fveq2	$⊢ g = G \to iEdg (g) = iEdg (G)$
7	6	adantr	$⊢ (g = G \land s = S) \to iEdg (g) = iEdg (G)$
8	7	adantr	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to iEdg (g) = iEdg (G)$
9	5 8	eqtrd	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to i = iEdg (G)$
10	9	dmeqd	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to dom i = dom iEdg (G)$
11		wrdeq	$⊢ dom i = dom iEdg (G) \to Word dom i = Word dom iEdg (G)$
12	10 11	syl	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to Word dom i = Word dom iEdg (G)$
13	12	eleq2d	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to (f \in Word dom i \leftrightarrow f \in Word dom iEdg (G))$
14		simpr	$⊢ (g = G \land s = S) \to s = S$
15	14	adantr	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to s = S$
16	9	fveq1d	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to i (f (k - 1)) = iEdg (G) (f (k - 1))$
17	9	fveq1d	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to i (f (k)) = iEdg (G) (f (k))$
18	16 17	ineq12d	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to i (f (k - 1)) \cap i (f (k)) = iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))$
19	18	fveq2d	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to \|i (f (k - 1)) \cap i (f (k))\| = \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|$
20	15 19	breq12d	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to (s \leq \|i (f (k - 1)) \cap i (f (k))\| \leftrightarrow S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)$
21	20	ralbidv	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \to (\forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\| \leftrightarrow \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)$
22	13 21	anbi12d	$⊢ ((g = G \land s = S) \land i = iEdg (g)) \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 iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|))$
23	4 22	sbcied	$⊢ (g = G \land s = S) \to (\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))\|) \leftrightarrow (f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|))$
24	23	abbidv	$⊢ (g = G \land s = S) \to \{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))\|)\} = \{f \| (f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)\}$
25	24	adantl	$⊢ ((G \in W \land S \in ℕ_{0}^{*}) \land (g = G \land s = S)) \to \{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))\|)\} = \{f \| (f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)\}$
26		elex	$⊢ G \in W \to G \in V$
27	26	adantr	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to G \in V$
28		simpr	$⊢ (G \in W \land S \in ℕ_{0}^{}) \to S \in ℕ_{0}^{}$
29		df-rab	$⊢ \{f \in Word dom iEdg (G) \| \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|\} = \{f \| (f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)\}$
30		fvex	$⊢ iEdg (G) \in V$
31	30	dmex	$⊢ dom iEdg (G) \in V$
32	31	wrdexi	$⊢ Word dom iEdg (G) \in V$
33	32	rabex	$⊢ \{f \in Word dom iEdg (G) \| \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|\} \in V$
34	33	a1i	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to \{f \in Word dom iEdg (G) \| \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|\} \in V$
35	29 34	eqeltrrid	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to \{f \| (f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)\} \in V$
36	3 25 27 28 35	ovmpod	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to G EdgWalks S = \{f \| (f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)\}$
37	1	eqcomi	$⊢ iEdg (G) = I$
38	37	a1i	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to iEdg (G) = I$
39	38	dmeqd	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to dom iEdg (G) = dom I$
40		wrdeq	$⊢ dom iEdg (G) = dom I \to Word dom iEdg (G) = Word dom I$
41	39 40	syl	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to Word dom iEdg (G) = Word dom I$
42	41	eleq2d	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to (f \in Word dom iEdg (G) \leftrightarrow f \in Word dom I)$
43	38	fveq1d	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to iEdg (G) (f (k - 1)) = I (f (k - 1))$
44	38	fveq1d	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to iEdg (G) (f (k)) = I (f (k))$
45	43 44	ineq12d	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k)) = I (f (k - 1)) \cap I (f (k))$
46	45	fveq2d	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\| = \|I (f (k - 1)) \cap I (f (k))\|$
47	46	breq2d	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to (S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\| \leftrightarrow S \leq \|I (f (k - 1)) \cap I (f (k))\|)$
48	47	ralbidv	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to (\forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\| \leftrightarrow \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|)$
49	42 48	anbi12d	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to ((f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|) \leftrightarrow (f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|))$
50	49	abbidv	$⊢ (G \in W \land S \in ℕ_{0}^{*}) \to \{f \| (f \in Word dom iEdg (G) \land \forall k \in (1 ..^\|f\|) S \leq \|iEdg (G) (f (k - 1)) \cap iEdg (G) (f (k))\|)\} = \{f \| (f \in Word dom I \land \forall k \in (1 ..^\|f\|) S \leq \|I (f (k - 1)) \cap I (f (k))\|)\}$
51	36 50	eqtrd	$⊢ (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))\|)\}$

Metamath Proof Explorer

Theorem ewlksfval

Proof