fusgreg2wsp

Description: In a finite simple graph, the set of all paths of length 2 is the union of all the paths of length 2 over the vertices which are in the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 18-May-2021) (Proof shortened by AV, 10-Jan-2022)

	Ref	Expression
Hypotheses	frgrhash2wsp.v	$⊢ V = Vtx (G)$
	fusgreg2wsp.m	$⊢ M = (a \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
Assertion	fusgreg2wsp	$⊢ G \in FinUSGraph \to 2 WSPathsN G = ⋃_{x \in V} M (x)$

Proof

Step	Hyp	Ref	Expression
1		frgrhash2wsp.v	$⊢ V = Vtx (G)$
2		fusgreg2wsp.m	$⊢ M = (a \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
3		wspthsswwlkn	$⊢ 2 WSPathsN G \subseteq 2 WWalksN G$
4	3	sseli	$⊢ p \in (2 WSPathsN G) \to p \in (2 WWalksN G)$
5	1	midwwlks2s3	$⊢ p \in (2 WWalksN G) \to \exists x \in V p (1) = x$
6	4 5	syl	$⊢ p \in (2 WSPathsN G) \to \exists x \in V p (1) = x$
7	6	a1i	$⊢ G \in FinUSGraph \to (p \in (2 WSPathsN G) \to \exists x \in V p (1) = x)$
8	7	pm4.71rd	$⊢ G \in FinUSGraph \to (p \in (2 WSPathsN G) \leftrightarrow (\exists x \in V p (1) = x \land p \in (2 WSPathsN G)))$
9		ancom	$⊢ (p \in (2 WSPathsN G) \land p (1) = x) \leftrightarrow (p (1) = x \land p \in (2 WSPathsN G))$
10	9	rexbii	$⊢ \exists x \in V (p \in (2 WSPathsN G) \land p (1) = x) \leftrightarrow \exists x \in V (p (1) = x \land p \in (2 WSPathsN G))$
11		r19.41v	$⊢ \exists x \in V (p (1) = x \land p \in (2 WSPathsN G)) \leftrightarrow (\exists x \in V p (1) = x \land p \in (2 WSPathsN G))$
12	10 11	bitr2i	$⊢ (\exists x \in V p (1) = x \land p \in (2 WSPathsN G)) \leftrightarrow \exists x \in V (p \in (2 WSPathsN G) \land p (1) = x)$
13	12	a1i	$⊢ G \in FinUSGraph \to ((\exists x \in V p (1) = x \land p \in (2 WSPathsN G)) \leftrightarrow \exists x \in V (p \in (2 WSPathsN G) \land p (1) = x))$
14	1 2	fusgreg2wsplem	$⊢ x \in V \to (p \in M (x) \leftrightarrow (p \in (2 WSPathsN G) \land p (1) = x))$
15	14	bicomd	$⊢ x \in V \to ((p \in (2 WSPathsN G) \land p (1) = x) \leftrightarrow p \in M (x))$
16	15	adantl	$⊢ (G \in FinUSGraph \land x \in V) \to ((p \in (2 WSPathsN G) \land p (1) = x) \leftrightarrow p \in M (x))$
17	16	rexbidva	$⊢ G \in FinUSGraph \to (\exists x \in V (p \in (2 WSPathsN G) \land p (1) = x) \leftrightarrow \exists x \in V p \in M (x))$
18	8 13 17	3bitrd	$⊢ G \in FinUSGraph \to (p \in (2 WSPathsN G) \leftrightarrow \exists x \in V p \in M (x))$
19		eliun	$⊢ p \in ⋃_{x \in V} M (x) \leftrightarrow \exists x \in V p \in M (x)$
20	18 19	bitr4di	$⊢ G \in FinUSGraph \to (p \in (2 WSPathsN G) \leftrightarrow p \in ⋃_{x \in V} M (x))$
21	20	eqrdv	$⊢ G \in FinUSGraph \to 2 WSPathsN G = ⋃_{x \in V} M (x)$

Metamath Proof Explorer

Theorem fusgreg2wsp

Proof