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		wksv	$⊢ \{⟨f, p⟩ \| f Walks (G) p\} \in V$
9	8	a1i	$⊢ (A \in V \land B \in V) \to \{⟨f, p⟩ \| f Walks (G) p\} \in V$
10		simpr	$⊢ ((A \in V \land B \in V) \land f Walks (G) p) \to f Walks (G) p$
11		eqeq2	$⊢ a = A \to (p (0) = a \leftrightarrow p (0) = A)$
12		eqeq2	$⊢ b = B \to (p (\|f\|) = b \leftrightarrow p (\|f\|) = B)$
13	11 12	bi2anan9	$⊢ (a = A \land b = B) \to ((p (0) = a \land p (\|f\|) = b) \leftrightarrow (p (0) = A \land p (\|f\|) = B))$
14		biidd	$⊢ g = G \to ((p (0) = a \land p (\|f\|) = b) \leftrightarrow (p (0) = a \land p (\|f\|) = b))$
15		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)\}))$
16		eqid	$⊢ Vtx (g) = Vtx (g)$
17		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))$
18	17	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)$
19	18	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)\}$
20	16 16 19	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)\})$
21	20	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)\}))$
22	15 21	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)\}))$
23	3 5 7 9 10 13 14 22	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)\}$
24		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))$
25		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))$
26	24 25	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)$
27	26	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)\}$
28	23 27	syl6eq	$⊢ (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