wlkonprop

Description: Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 31-Dec-2020) (Proof shortened by AV, 16-Jan-2021)

		Ref	Expression
	Hypothesis	wlkson.v	$⊢ V = Vtx (G)$
	Assertion	wlkonprop	$⊢ F (A WalksOn (G) B) P \to ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V) \land (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	fvexi	$⊢ V \in V$
3		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)\}))$
4	1	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)\}$
5	4	3adant1	$⊢ (G \in V \land 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)\}$
6		fveq2	$⊢ g = G \to Vtx (g) = Vtx (G)$
7	6 1	eqtr4di	$⊢ g = G \to Vtx (g) = V$
8		fveq2	$⊢ g = G \to Walks (g) = Walks (G)$
9	8	breqd	$⊢ g = G \to (f Walks (g) p \leftrightarrow f Walks (G) p)$
10	9	3anbi1d	$⊢ g = G \to ((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))$
11	3 5 7 7 10	bropfvvvv	$⊢ (V \in V \land V \in V) \to (F (A WalksOn (G) B) P \to (G \in V \land (A \in V \land B \in V) \land (F \in V \land P \in V)))$
12	2 2 11	mp2an	$⊢ F (A WalksOn (G) B) P \to (G \in V \land (A \in V \land B \in V) \land (F \in V \land P \in V))$
13		3anass	$⊢ (G \in V \land A \in V \land B \in V) \leftrightarrow (G \in V \land (A \in V \land B \in V))$
14	13	anbi1i	$⊢ ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \leftrightarrow ((G \in V \land (A \in V \land B \in V)) \land (F \in V \land P \in V))$
15		df-3an	$⊢ (G \in V \land (A \in V \land B \in V) \land (F \in V \land P \in V)) \leftrightarrow ((G \in V \land (A \in V \land B \in V)) \land (F \in V \land P \in V))$
16	14 15	bitr4i	$⊢ ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \leftrightarrow (G \in V \land (A \in V \land B \in V) \land (F \in V \land P \in V))$
17	12 16	sylibr	$⊢ F (A WalksOn (G) B) P \to ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V))$
18	1	iswlkon	$⊢ ((A \in V \land B \in V) \land (F \in V \land P \in V)) \to (F (A WalksOn (G) B) P \leftrightarrow (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
19	18	3adantl1	$⊢ ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \to (F (A WalksOn (G) B) P \leftrightarrow (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
20	19	biimpd	$⊢ ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \to (F (A WalksOn (G) B) P \to (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
21	20	imdistani	$⊢ (((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \land F (A WalksOn (G) B) P) \to (((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
22	17 21	mpancom	$⊢ F (A WalksOn (G) B) P \to (((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
23		df-3an	$⊢ ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B)) \leftrightarrow (((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V)) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
24	22 23	sylibr	$⊢ F (A WalksOn (G) B) P \to ((G \in V \land A \in V \land B \in V) \land (F \in V \land P \in V) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$

Metamath Proof Explorer

Theorem wlkonprop

Proof