2wspmdisj

Description: The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-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	2wspmdisj	$⊢ \underset{x \in V}{Disj} 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		orc	$⊢ x = y \to (x = y \lor M (x) \cap M (y) = \emptyset)$
4	3	a1d	$⊢ x = y \to ((x \in V \land y \in V) \to (x = y \lor M (x) \cap M (y) = \emptyset))$
5	1 2	fusgreg2wsplem	$⊢ y \in V \to (t \in M (y) \leftrightarrow (t \in (2 WSPathsN G) \land t (1) = y))$
6	5	adantl	$⊢ (x \in V \land y \in V) \to (t \in M (y) \leftrightarrow (t \in (2 WSPathsN G) \land t (1) = y))$
7	6	adantr	$⊢ ((x \in V \land y \in V) \land t \in M (x)) \to (t \in M (y) \leftrightarrow (t \in (2 WSPathsN G) \land t (1) = y))$
8	1 2	fusgreg2wsplem	$⊢ x \in V \to (t \in M (x) \leftrightarrow (t \in (2 WSPathsN G) \land t (1) = x))$
9		eqtr2	$⊢ (t (1) = x \land t (1) = y) \to x = y$
10	9	expcom	$⊢ t (1) = y \to (t (1) = x \to x = y)$
11	10	adantl	$⊢ (t \in (2 WSPathsN G) \land t (1) = y) \to (t (1) = x \to x = y)$
12	11	com12	$⊢ t (1) = x \to ((t \in (2 WSPathsN G) \land t (1) = y) \to x = y)$
13	12	adantl	$⊢ (t \in (2 WSPathsN G) \land t (1) = x) \to ((t \in (2 WSPathsN G) \land t (1) = y) \to x = y)$
14	8 13	syl6bi	$⊢ x \in V \to (t \in M (x) \to ((t \in (2 WSPathsN G) \land t (1) = y) \to x = y))$
15	14	adantr	$⊢ (x \in V \land y \in V) \to (t \in M (x) \to ((t \in (2 WSPathsN G) \land t (1) = y) \to x = y))$
16	15	imp	$⊢ ((x \in V \land y \in V) \land t \in M (x)) \to ((t \in (2 WSPathsN G) \land t (1) = y) \to x = y)$
17	7 16	sylbid	$⊢ ((x \in V \land y \in V) \land t \in M (x)) \to (t \in M (y) \to x = y)$
18	17	con3d	$⊢ ((x \in V \land y \in V) \land t \in M (x)) \to (\neg x = y \to \neg t \in M (y))$
19	18	impancom	$⊢ ((x \in V \land y \in V) \land \neg x = y) \to (t \in M (x) \to \neg t \in M (y))$
20	19	ralrimiv	$⊢ ((x \in V \land y \in V) \land \neg x = y) \to \forall t \in M (x) \neg t \in M (y)$
21		disj	$⊢ M (x) \cap M (y) = \emptyset \leftrightarrow \forall t \in M (x) \neg t \in M (y)$
22	20 21	sylibr	$⊢ ((x \in V \land y \in V) \land \neg x = y) \to M (x) \cap M (y) = \emptyset$
23	22	olcd	$⊢ ((x \in V \land y \in V) \land \neg x = y) \to (x = y \lor M (x) \cap M (y) = \emptyset)$
24	23	expcom	$⊢ \neg x = y \to ((x \in V \land y \in V) \to (x = y \lor M (x) \cap M (y) = \emptyset))$
25	4 24	pm2.61i	$⊢ (x \in V \land y \in V) \to (x = y \lor M (x) \cap M (y) = \emptyset)$
26	25	rgen2	$⊢ \forall x \in V \forall y \in V (x = y \lor M (x) \cap M (y) = \emptyset)$
27		fveq2	$⊢ x = y \to M (x) = M (y)$
28	27	disjor	$⊢ \underset{x \in V}{Disj} M (x) \leftrightarrow \forall x \in V \forall y \in V (x = y \lor M (x) \cap M (y) = \emptyset)$
29	26 28	mpbir	$⊢ \underset{x \in V}{Disj} M (x)$

Metamath Proof Explorer

Theorem 2wspmdisj

Proof