wwlksnextprop

Description: Adding additional properties to the set of walks (as words) of a fixed length starting at a fixed vertex. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-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	wwlksnextprop	$⊢ N \in ℕ_{0} \to \{x \in X \| x (0) = P\} = \{x \in X \| \exists y \in Y (x prefix (N + 1) = 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		eqidd	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to x prefix (N + 1) = x prefix (N + 1)$
5	1	wwlksnextproplem1	$⊢ (x \in X \land N \in ℕ_{0}) \to (x prefix (N + 1)) (0) = x (0)$
6	5	ancoms	$⊢ (N \in ℕ_{0} \land x \in X) \to (x prefix (N + 1)) (0) = x (0)$
7	6	adantr	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to (x prefix (N + 1)) (0) = x (0)$
8		eqeq2	$⊢ x (0) = P \to ((x prefix (N + 1)) (0) = x (0) \leftrightarrow (x prefix (N + 1)) (0) = P)$
9	8	adantl	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to ((x prefix (N + 1)) (0) = x (0) \leftrightarrow (x prefix (N + 1)) (0) = P)$
10	7 9	mpbid	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to (x prefix (N + 1)) (0) = P$
11	1 2	wwlksnextproplem2	$⊢ (x \in X \land N \in ℕ_{0}) \to \{lastS (x prefix (N + 1)), lastS (x)\} \in E$
12	11	ancoms	$⊢ (N \in ℕ_{0} \land x \in X) \to \{lastS (x prefix (N + 1)), lastS (x)\} \in E$
13	12	adantr	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to \{lastS (x prefix (N + 1)), lastS (x)\} \in E$
14		simpr	$⊢ (N \in ℕ_{0} \land x \in X) \to x \in X$
15	14	adantr	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to x \in X$
16		simpr	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to x (0) = P$
17		simpll	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to N \in ℕ_{0}$
18	1 2 3	wwlksnextproplem3	$⊢ (x \in X \land x (0) = P \land N \in ℕ_{0}) \to x prefix (N + 1) \in Y$
19	15 16 17 18	syl3anc	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to x prefix (N + 1) \in Y$
20		eqeq2	$⊢ y = x prefix (N + 1) \to (x prefix (N + 1) = y \leftrightarrow x prefix (N + 1) = x prefix (N + 1))$
21		fveq1	$⊢ y = x prefix (N + 1) \to y (0) = (x prefix (N + 1)) (0)$
22	21	eqeq1d	$⊢ y = x prefix (N + 1) \to (y (0) = P \leftrightarrow (x prefix (N + 1)) (0) = P)$
23		fveq2	$⊢ y = x prefix (N + 1) \to lastS (y) = lastS (x prefix (N + 1))$
24	23	preq1d	$⊢ y = x prefix (N + 1) \to \{lastS (y), lastS (x)\} = \{lastS (x prefix (N + 1)), lastS (x)\}$
25	24	eleq1d	$⊢ y = x prefix (N + 1) \to (\{lastS (y), lastS (x)\} \in E \leftrightarrow \{lastS (x prefix (N + 1)), lastS (x)\} \in E)$
26	20 22 25	3anbi123d	$⊢ y = x prefix (N + 1) \to ((x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \leftrightarrow (x prefix (N + 1) = x prefix (N + 1) \land (x prefix (N + 1)) (0) = P \land \{lastS (x prefix (N + 1)), lastS (x)\} \in E))$
27	26	adantl	$⊢ (((N \in ℕ_{0} \land x \in X) \land x (0) = P) \land y = x prefix (N + 1)) \to ((x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \leftrightarrow (x prefix (N + 1) = x prefix (N + 1) \land (x prefix (N + 1)) (0) = P \land \{lastS (x prefix (N + 1)), lastS (x)\} \in E))$
28	19 27	rspcedv	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to ((x prefix (N + 1) = x prefix (N + 1) \land (x prefix (N + 1)) (0) = P \land \{lastS (x prefix (N + 1)), lastS (x)\} \in E) \to \exists y \in Y (x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E))$
29	4 10 13 28	mp3and	$⊢ ((N \in ℕ_{0} \land x \in X) \land x (0) = P) \to \exists y \in Y (x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)$
30	29	ex	$⊢ (N \in ℕ_{0} \land x \in X) \to (x (0) = P \to \exists y \in Y (x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E))$
31	21	eqcoms	$⊢ x prefix (N + 1) = y \to y (0) = (x prefix (N + 1)) (0)$
32	31	eqeq1d	$⊢ x prefix (N + 1) = y \to (y (0) = P \leftrightarrow (x prefix (N + 1)) (0) = P)$
33	5	eqcomd	$⊢ (x \in X \land N \in ℕ_{0}) \to x (0) = (x prefix (N + 1)) (0)$
34	33	ancoms	$⊢ (N \in ℕ_{0} \land x \in X) \to x (0) = (x prefix (N + 1)) (0)$
35	34	adantr	$⊢ ((N \in ℕ_{0} \land x \in X) \land y \in Y) \to x (0) = (x prefix (N + 1)) (0)$
36		eqeq2	$⊢ P = (x prefix (N + 1)) (0) \to (x (0) = P \leftrightarrow x (0) = (x prefix (N + 1)) (0))$
37	36	eqcoms	$⊢ (x prefix (N + 1)) (0) = P \to (x (0) = P \leftrightarrow x (0) = (x prefix (N + 1)) (0))$
38	35 37	imbitrrid	$⊢ (x prefix (N + 1)) (0) = P \to (((N \in ℕ_{0} \land x \in X) \land y \in Y) \to x (0) = P)$
39	32 38	syl6bi	$⊢ x prefix (N + 1) = y \to (y (0) = P \to (((N \in ℕ_{0} \land x \in X) \land y \in Y) \to x (0) = P))$
40	39	imp	$⊢ (x prefix (N + 1) = y \land y (0) = P) \to (((N \in ℕ_{0} \land x \in X) \land y \in Y) \to x (0) = P)$
41	40	3adant3	$⊢ (x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \to (((N \in ℕ_{0} \land x \in X) \land y \in Y) \to x (0) = P)$
42	41	com12	$⊢ ((N \in ℕ_{0} \land x \in X) \land y \in Y) \to ((x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \to x (0) = P)$
43	42	rexlimdva	$⊢ (N \in ℕ_{0} \land x \in X) \to (\exists y \in Y (x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E) \to x (0) = P)$
44	30 43	impbid	$⊢ (N \in ℕ_{0} \land x \in X) \to (x (0) = P \leftrightarrow \exists y \in Y (x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E))$
45	44	rabbidva	$⊢ N \in ℕ_{0} \to \{x \in X \| x (0) = P\} = \{x \in X \| \exists y \in Y (x prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (x)\} \in E)\}$

Metamath Proof Explorer

Theorem wwlksnextprop

Proof