wlkson

Description: The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 30-Dec-2020) (Revised by AV, 22-Mar-2021)

		Ref	Expression
	Hypothesis	wlkson.v	$⊢ V = Vtx (G)$
	Assertion	wlkson	$⊢ (A \in V \land B \in V) \to A WalksOn (G) B = \{⟨f, p⟩ \| (f Walks (G) p \land p (0) = A \land p (\|f\|) = B)\}$

Proof

Step	Hyp	Ref	Expression
1		wlkson.v	$⊢ V = Vtx (G)$
2	1	1vgrex	$⊢ A \in V \to G \in V$
3	2	adantr	$⊢ (A \in V \land B \in V) \to G \in V$
4		simpl	$⊢ (A \in V \land B \in V) \to A \in V$
5	4 1	eleqtrdi	$⊢ (A \in V \land B \in V) \to A \in Vtx (G)$
6		simpr	$⊢ (A \in V \land B \in V) \to B \in V$
7	6 1	eleqtrdi	$⊢ (A \in V \land B \in V) \to B \in Vtx (G)$
8		eqeq2	$⊢ a = A \to (p (0) = a \leftrightarrow p (0) = A)$
9		eqeq2	$⊢ b = B \to (p (\|f\|) = b \leftrightarrow p (\|f\|) = B)$
10	8 9	bi2anan9	$⊢ (a = A \land b = B) \to ((p (0) = a \land p (\|f\|) = b) \leftrightarrow (p (0) = A \land p (\|f\|) = B))$
11		biidd	$⊢ g = G \to ((p (0) = a \land p (\|f\|) = b) \leftrightarrow (p (0) = a \land p (\|f\|) = b))$
12		df-wlkson	$⊢ WalksOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\}))$
13		eqid	$⊢ Vtx (g) = Vtx (g)$
14		3anass	$⊢ (f Walks (g) p \land p (0) = a \land p (\|f\|) = b) \leftrightarrow (f Walks (g) p \land (p (0) = a \land p (\|f\|) = b))$
15	14	biancomi	$⊢ (f Walks (g) p \land p (0) = a \land p (\|f\|) = b) \leftrightarrow ((p (0) = a \land p (\|f\|) = b) \land f Walks (g) p)$
16	15	opabbii	$⊢ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\} = \{⟨f, p⟩ \| ((p (0) = a \land p (\|f\|) = b) \land f Walks (g) p)\}$
17	13 13 16	mpoeq123i	$⊢ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\}) = (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| ((p (0) = a \land p (\|f\|) = b) \land f Walks (g) p)\})$
18	17	mpteq2i	$⊢ (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\})) = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| ((p (0) = a \land p (\|f\|) = b) \land f Walks (g) p)\}))$
19	12 18	eqtri	$⊢ WalksOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| ((p (0) = a \land p (\|f\|) = b) \land f Walks (g) p)\}))$
20	3 5 7 10 11 19	mptmpoopabbrd	$⊢ (A \in V \land B \in V) \to A WalksOn (G) B = \{⟨f, p⟩ \| ((p (0) = A \land p (\|f\|) = B) \land f Walks (G) p)\}$
21		ancom	$⊢ ((p (0) = A \land p (\|f\|) = B) \land f Walks (G) p) \leftrightarrow (f Walks (G) p \land (p (0) = A \land p (\|f\|) = B))$
22		3anass	$⊢ (f Walks (G) p \land p (0) = A \land p (\|f\|) = B) \leftrightarrow (f Walks (G) p \land (p (0) = A \land p (\|f\|) = B))$
23	21 22	bitr4i	$⊢ ((p (0) = A \land p (\|f\|) = B) \land f Walks (G) p) \leftrightarrow (f Walks (G) p \land p (0) = A \land p (\|f\|) = B)$
24	23	opabbii	$⊢ \{⟨f, p⟩ \| ((p (0) = A \land p (\|f\|) = B) \land f Walks (G) p)\} = \{⟨f, p⟩ \| (f Walks (G) p \land p (0) = A \land p (\|f\|) = B)\}$
25	20 24	eqtrdi	$⊢ (A \in V \land B \in V) \to A WalksOn (G) B = \{⟨f, p⟩ \| (f Walks (G) p \land p (0) = A \land p (\|f\|) = B)\}$

Metamath Proof Explorer

Theorem wlkson

Proof