Metamath Proof Explorer

Theorem disjxwwlkn

Description: Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 26-Oct-2022)

		Ref	Expression
	Hypotheses	wwlksnextprop.x	$⊢ X = (N + 1) WWalksN G$
		wwlksnextprop.e	$⊢ E = Edg (G)$
		wwlksnextprop.y	$⊢ Y = \{w \in (N WWalksN G) \| w (0) = P\}$
	Assertion	disjxwwlkn	$⊢ \underset{y \in Y}{Disj} \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\}$

Proof

Step	Hyp	Ref	Expression
1		wwlksnextprop.x	$⊢ X = (N + 1) WWalksN G$
2		wwlksnextprop.e	$⊢ E = Edg (G)$
3		wwlksnextprop.y	$⊢ Y = \{w \in (N WWalksN G) \| w (0) = P\}$
4		simp1	$⊢ (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \to x prefix M = y$
5	4	rgenw	$⊢ \forall x \in X ((x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \to x prefix M = y)$
6		ss2rab	$⊢ \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\} \subseteq \{x \in X \| x prefix M = y\} \leftrightarrow \forall x \in X ((x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \to x prefix M = y)$
7	5 6	mpbir	$⊢ \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\} \subseteq \{x \in X \| x prefix M = y\}$
8		wwlkssswwlksn	$⊢ (N + 1) WWalksN G \subseteq WWalks (G)$
9		eqid	$⊢ Vtx (G) = Vtx (G)$
10	9	wwlkssswrd	$⊢ WWalks (G) \subseteq Word Vtx (G)$
11	8 10	sstri	$⊢ (N + 1) WWalksN G \subseteq Word Vtx (G)$
12	1 11	eqsstri	$⊢ X \subseteq Word Vtx (G)$
13		rabss2	$⊢ X \subseteq Word Vtx (G) \to \{x \in X \| x prefix M = y\} \subseteq \{x \in Word Vtx (G) \| x prefix M = y\}$
14	12 13	ax-mp	$⊢ \{x \in X \| x prefix M = y\} \subseteq \{x \in Word Vtx (G) \| x prefix M = y\}$
15	7 14	sstri	$⊢ \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\} \subseteq \{x \in Word Vtx (G) \| x prefix M = y\}$
16	15	rgenw	$⊢ \forall y \in Y \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\} \subseteq \{x \in Word Vtx (G) \| x prefix M = y\}$
17		disjwrdpfx	$⊢ \underset{y \in Y}{Disj} \{x \in Word Vtx (G) \| x prefix M = y\}$
18		disjss2	$⊢ \forall y \in Y \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\} \subseteq \{x \in Word Vtx (G) \| x prefix M = y\} \to (\underset{y \in Y}{Disj} \{x \in Word Vtx (G) \| x prefix M = y\} \to \underset{y \in Y}{Disj} \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\})$
19	16 17 18	mp2	$⊢ \underset{y \in Y}{Disj} \{x \in X \| (x prefix M = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\}$