wspniunwspnon

Description: The set of nonempty simple paths of fixed length is the double union of the simple paths of the fixed length between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018) (Revised by AV, 16-May-2021) (Proof shortened by AV, 15-Mar-2022)

		Ref	Expression
	Hypothesis	wspniunwspnon.v	$⊢ V = Vtx (G)$
	Assertion	wspniunwspnon	$⊢ (N \in ℕ \land G \in U) \to N WSPathsN G = ⋃_{x \in V} ⋃_{y \in V ∖ \{x\}} (x (N WSPathsNOn G) y)$

Proof

Step	Hyp	Ref	Expression
1		wspniunwspnon.v	$⊢ V = Vtx (G)$
2		wspthsnonn0vne	$⊢ (N \in ℕ \land x (N WSPathsNOn G) y \neq \emptyset) \to x \neq y$
3	2	ex	$⊢ N \in ℕ \to (x (N WSPathsNOn G) y \neq \emptyset \to x \neq y)$
4	3	adantr	$⊢ (N \in ℕ \land G \in U) \to (x (N WSPathsNOn G) y \neq \emptyset \to x \neq y)$
5		ne0i	$⊢ w \in (x (N WSPathsNOn G) y) \to x (N WSPathsNOn G) y \neq \emptyset$
6	4 5	impel	$⊢ ((N \in ℕ \land G \in U) \land w \in (x (N WSPathsNOn G) y)) \to x \neq y$
7	6	necomd	$⊢ ((N \in ℕ \land G \in U) \land w \in (x (N WSPathsNOn G) y)) \to y \neq x$
8	7	ex	$⊢ (N \in ℕ \land G \in U) \to (w \in (x (N WSPathsNOn G) y) \to y \neq x)$
9	8	pm4.71rd	$⊢ (N \in ℕ \land G \in U) \to (w \in (x (N WSPathsNOn G) y) \leftrightarrow (y \neq x \land w \in (x (N WSPathsNOn G) y)))$
10	9	rexbidv	$⊢ (N \in ℕ \land G \in U) \to (\exists y \in V w \in (x (N WSPathsNOn G) y) \leftrightarrow \exists y \in V (y \neq x \land w \in (x (N WSPathsNOn G) y)))$
11		rexdifsn	$⊢ \exists y \in (V ∖ \{x\}) w \in (x (N WSPathsNOn G) y) \leftrightarrow \exists y \in V (y \neq x \land w \in (x (N WSPathsNOn G) y))$
12	10 11	bitr4di	$⊢ (N \in ℕ \land G \in U) \to (\exists y \in V w \in (x (N WSPathsNOn G) y) \leftrightarrow \exists y \in (V ∖ \{x\}) w \in (x (N WSPathsNOn G) y))$
13	12	rexbidv	$⊢ (N \in ℕ \land G \in U) \to (\exists x \in V \exists y \in V w \in (x (N WSPathsNOn G) y) \leftrightarrow \exists x \in V \exists y \in (V ∖ \{x\}) w \in (x (N WSPathsNOn G) y))$
14	1	wspthsnwspthsnon	$⊢ w \in (N WSPathsN G) \leftrightarrow \exists x \in V \exists y \in V w \in (x (N WSPathsNOn G) y)$
15		vex	$⊢ w \in V$
16		eleq1w	$⊢ p = w \to (p \in (x (N WSPathsNOn G) y) \leftrightarrow w \in (x (N WSPathsNOn G) y))$
17	16	rexbidv	$⊢ p = w \to (\exists y \in (V ∖ \{x\}) p \in (x (N WSPathsNOn G) y) \leftrightarrow \exists y \in (V ∖ \{x\}) w \in (x (N WSPathsNOn G) y))$
18	17	rexbidv	$⊢ p = w \to (\exists x \in V \exists y \in (V ∖ \{x\}) p \in (x (N WSPathsNOn G) y) \leftrightarrow \exists x \in V \exists y \in (V ∖ \{x\}) w \in (x (N WSPathsNOn G) y))$
19	15 18	elab	$⊢ w \in \{p \| \exists x \in V \exists y \in (V ∖ \{x\}) p \in (x (N WSPathsNOn G) y)\} \leftrightarrow \exists x \in V \exists y \in (V ∖ \{x\}) w \in (x (N WSPathsNOn G) y)$
20	13 14 19	3bitr4g	$⊢ (N \in ℕ \land G \in U) \to (w \in (N WSPathsN G) \leftrightarrow w \in \{p \| \exists x \in V \exists y \in (V ∖ \{x\}) p \in (x (N WSPathsNOn G) y)\})$
21	20	eqrdv	$⊢ (N \in ℕ \land G \in U) \to N WSPathsN G = \{p \| \exists x \in V \exists y \in (V ∖ \{x\}) p \in (x (N WSPathsNOn G) y)\}$
22		dfiunv2	$⊢ ⋃_{x \in V} ⋃_{y \in V ∖ \{x\}} (x (N WSPathsNOn G) y) = \{p \| \exists x \in V \exists y \in (V ∖ \{x\}) p \in (x (N WSPathsNOn G) y)\}$
23	21 22	eqtr4di	$⊢ (N \in ℕ \land G \in U) \to N WSPathsN G = ⋃_{x \in V} ⋃_{y \in V ∖ \{x\}} (x (N WSPathsNOn G) y)$

Metamath Proof Explorer

Theorem wspniunwspnon

Proof