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=\left(N+1\right)\mathrm{WWalksN}G$$
	wwlksnextprop.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
	wwlksnextprop.y	$$⊢Y=\left\{w\in \left(N\mathrm{WWalksN}G\right)|w\left(0\right)=P\right\}$$
Assertion	disjxwwlkn	$$⊢\underset{y\in Y}{Disj}\left\{x\in X|\left(x\mathrm{prefix}M=y\wedge y\left(0\right)=P\wedge \left\{\mathrm{lastS}\left(y\right),\mathrm{lastS}\left(x\right)\right\}\in E\right)\right\}$$

Proof

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