Metamath Proof Explorer

Theorem clwwlknondisj

Description: The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 28-May-2021) (Revised by AV, 3-Mar-2022) (Proof shortened by AV, 28-Mar-2022)

		Ref	Expression
	Assertion	clwwlknondisj	$⊢ \underset{x \in V}{Disj} (x ClWWalksNOn (G) N)$

Proof

Step	Hyp	Ref	Expression
1		clwwlknon	$⊢ x ClWWalksNOn (G) N = \{w \in (N ClWWalksN G) \| w (0) = x\}$
2		clwwlknon	$⊢ y ClWWalksNOn (G) N = \{w \in (N ClWWalksN G) \| w (0) = y\}$
3	1 2	ineq12i	$⊢ (x ClWWalksNOn (G) N) \cap (y ClWWalksNOn (G) N) = \{w \in (N ClWWalksN G) \| w (0) = x\} \cap \{w \in (N ClWWalksN G) \| w (0) = y\}$
4		inrab	$⊢ \{w \in (N ClWWalksN G) \| w (0) = x\} \cap \{w \in (N ClWWalksN G) \| w (0) = y\} = \{w \in (N ClWWalksN G) \| (w (0) = x \land w (0) = y)\}$
5		eqtr2	$⊢ (w (0) = x \land w (0) = y) \to x = y$
6	5	con3i	$⊢ \neg x = y \to \neg (w (0) = x \land w (0) = y)$
7	6	ralrimivw	$⊢ \neg x = y \to \forall w \in (N ClWWalksN G) \neg (w (0) = x \land w (0) = y)$
8		rabeq0	$⊢ \{w \in (N ClWWalksN G) \| (w (0) = x \land w (0) = y)\} = \emptyset \leftrightarrow \forall w \in (N ClWWalksN G) \neg (w (0) = x \land w (0) = y)$
9	7 8	sylibr	$⊢ \neg x = y \to \{w \in (N ClWWalksN G) \| (w (0) = x \land w (0) = y)\} = \emptyset$
10	4 9	eqtrid	$⊢ \neg x = y \to \{w \in (N ClWWalksN G) \| w (0) = x\} \cap \{w \in (N ClWWalksN G) \| w (0) = y\} = \emptyset$
11	3 10	eqtrid	$⊢ \neg x = y \to (x ClWWalksNOn (G) N) \cap (y ClWWalksNOn (G) N) = \emptyset$
12	11	orri	$⊢ (x = y \lor (x ClWWalksNOn (G) N) \cap (y ClWWalksNOn (G) N) = \emptyset)$
13	12	rgen2w	$⊢ \forall x \in V \forall y \in V (x = y \lor (x ClWWalksNOn (G) N) \cap (y ClWWalksNOn (G) N) = \emptyset)$
14		oveq1	$⊢ x = y \to x ClWWalksNOn (G) N = y ClWWalksNOn (G) N$
15	14	disjor	$⊢ \underset{x \in V}{Disj} (x ClWWalksNOn (G) N) \leftrightarrow \forall x \in V \forall y \in V (x = y \lor (x ClWWalksNOn (G) N) \cap (y ClWWalksNOn (G) N) = \emptyset)$
16	13 15	mpbir	$⊢ \underset{x \in V}{Disj} (x ClWWalksNOn (G) N)$