upwlksfval

Description: The set of simple walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017) (Revised by AV, 28-Dec-2020)

	Ref	Expression
Hypotheses	upwlksfval.v	$⊢ V = Vtx (G)$
	upwlksfval.i	$⊢ I = iEdg (G)$
Assertion	upwlksfval	$⊢ G \in W \to UPWalks (G) = \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\}$

Proof

Step	Hyp	Ref	Expression
1		upwlksfval.v	$⊢ V = Vtx (G)$
2		upwlksfval.i	$⊢ I = iEdg (G)$
3		df-upwlks	$⊢ UPWalks = (g \in V ⟼ \{⟨f, p⟩ \| (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) iEdg (g) (f (k)) = \{p (k), p (k + 1)\})\})$
4		fveq2	$⊢ g = G \to iEdg (g) = iEdg (G)$
5	4 2	eqtr4di	$⊢ g = G \to iEdg (g) = I$
6	5	dmeqd	$⊢ g = G \to dom iEdg (g) = dom I$
7		wrdeq	$⊢ dom iEdg (g) = dom I \to Word dom iEdg (g) = Word dom I$
8	6 7	syl	$⊢ g = G \to Word dom iEdg (g) = Word dom I$
9	8	eleq2d	$⊢ g = G \to (f \in Word dom iEdg (g) \leftrightarrow f \in Word dom I)$
10		fveq2	$⊢ g = G \to Vtx (g) = Vtx (G)$
11	10 1	eqtr4di	$⊢ g = G \to Vtx (g) = V$
12	11	feq3d	$⊢ g = G \to (p : (0 \dots \|f\|) ⟶ Vtx (g) \leftrightarrow p : (0 \dots \|f\|) ⟶ V)$
13	5	fveq1d	$⊢ g = G \to iEdg (g) (f (k)) = I (f (k))$
14	13	eqeq1d	$⊢ g = G \to (iEdg (g) (f (k)) = \{p (k), p (k + 1)\} \leftrightarrow I (f (k)) = \{p (k), p (k + 1)\})$
15	14	ralbidv	$⊢ g = G \to (\forall k \in (0 ..^\|f\|) iEdg (g) (f (k)) = \{p (k), p (k + 1)\} \leftrightarrow \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})$
16	9 12 15	3anbi123d	$⊢ g = G \to ((f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) iEdg (g) (f (k)) = \{p (k), p (k + 1)\}) \leftrightarrow (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))$
17	16	opabbidv	$⊢ g = G \to \{⟨f, p⟩ \| (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) iEdg (g) (f (k)) = \{p (k), p (k + 1)\})\} = \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\}$
18		elex	$⊢ G \in W \to G \in V$
19		3anass	$⊢ (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}) \leftrightarrow (f \in Word dom I \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))$
20	19	opabbii	$⊢ \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\} = \{⟨f, p⟩ \| (f \in Word dom I \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))\}$
21	2	fvexi	$⊢ I \in V$
22	21	dmex	$⊢ dom I \in V$
23		wrdexg	$⊢ dom I \in V \to Word dom I \in V$
24	22 23	mp1i	$⊢ G \in W \to Word dom I \in V$
25		ovex	$⊢ (0 \dots \|f\|) \in V$
26	1	fvexi	$⊢ V \in V$
27	26	a1i	$⊢ (G \in W \land f \in Word dom I) \to V \in V$
28		mapex	$⊢ ((0 \dots \|f\|) \in V \land V \in V) \to \{p \| p : (0 \dots \|f\|) ⟶ V\} \in V$
29	25 27 28	sylancr	$⊢ (G \in W \land f \in Word dom I) \to \{p \| p : (0 \dots \|f\|) ⟶ V\} \in V$
30		simpl	$⊢ (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}) \to p : (0 \dots \|f\|) ⟶ V$
31	30	ss2abi	$⊢ \{p \| (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\} \subseteq \{p \| p : (0 \dots \|f\|) ⟶ V\}$
32	31	a1i	$⊢ (G \in W \land f \in Word dom I) \to \{p \| (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\} \subseteq \{p \| p : (0 \dots \|f\|) ⟶ V\}$
33	29 32	ssexd	$⊢ (G \in W \land f \in Word dom I) \to \{p \| (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\} \in V$
34	24 33	opabex3d	$⊢ G \in W \to \{⟨f, p⟩ \| (f \in Word dom I \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))\} \in V$
35	20 34	eqeltrid	$⊢ G \in W \to \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\} \in V$
36	3 17 18 35	fvmptd3	$⊢ G \in W \to UPWalks (G) = \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\}$

Metamath Proof Explorer

Theorem upwlksfval

Proof