wksfval

Description: The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020)

	Ref	Expression
Hypotheses	wksfval.v	$⊢ V = Vtx (G)$
	wksfval.i	$⊢ I = iEdg (G)$
Assertion	wksfval	$⊢ G \in W \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))))\}$

Proof

Step	Hyp	Ref	Expression
1		wksfval.v	$⊢ V = Vtx (G)$
2		wksfval.i	$⊢ I = iEdg (G)$
3		df-wlks	$⊢ Walks = (g \in V ⟼ \{⟨f, p⟩ \| (f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))))\})$
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)\} \leftrightarrow I (f (k)) = \{p (k)\})$
15	13	sseq2d	$⊢ g = G \to (\{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k)) \leftrightarrow \{p (k), p (k + 1)\} \subseteq I (f (k)))$
16	14 15	ifpbi23d	$⊢ g = G \to (if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))) \leftrightarrow if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))))$
17	16	ralbidv	$⊢ g = G \to (\forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))) \leftrightarrow \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))))$
18	9 12 17	3anbi123d	$⊢ g = G \to ((f \in Word dom iEdg (g) \land p : (0 \dots \|f\|) ⟶ Vtx (g) \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k)))) \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)))))$
19	18	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\|) if- (p (k) = p (k + 1), iEdg (g) (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq iEdg (g) (f (k))))\} = \{⟨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))))\}$
20		elex	$⊢ G \in W \to G \in V$
21		3anass	$⊢ (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)))) \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)))))$
22	21	opabbii	$⊢ \{⟨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))))\} = \{⟨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)))))\}$
23	2	fvexi	$⊢ I \in V$
24	23	dmex	$⊢ dom I \in V$
25		wrdexg	$⊢ dom I \in V \to Word dom I \in V$
26	24 25	mp1i	$⊢ G \in W \to Word dom I \in V$
27		ovex	$⊢ (0 \dots \|f\|) \in V$
28	1	fvexi	$⊢ V \in V$
29	28	a1i	$⊢ (G \in W \land f \in Word dom I) \to V \in V$
30		mapex	$⊢ ((0 \dots \|f\|) \in V \land V \in V) \to \{p \| p : (0 \dots \|f\|) ⟶ V\} \in V$
31	27 29 30	sylancr	$⊢ (G \in W \land f \in Word dom I) \to \{p \| p : (0 \dots \|f\|) ⟶ V\} \in V$
32		simpl	$⊢ (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)))) \to p : (0 \dots \|f\|) ⟶ V$
33	32	ss2abi	$⊢ \{p \| (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))))\} \subseteq \{p \| p : (0 \dots \|f\|) ⟶ V\}$
34	33	a1i	$⊢ (G \in W \land f \in Word dom I) \to \{p \| (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))))\} \subseteq \{p \| p : (0 \dots \|f\|) ⟶ V\}$
35	31 34	ssexd	$⊢ (G \in W \land f \in Word dom I) \to \{p \| (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))))\} \in V$
36	26 35	opabex3d	$⊢ G \in W \to \{⟨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)))))\} \in V$
37	22 36	eqeltrid	$⊢ G \in W \to \{⟨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))))\} \in V$
38	3 19 20 37	fvmptd3	$⊢ G \in W \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))))\}$

Metamath Proof Explorer

Theorem wksfval

Proof