wwlksnred

Description: Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021) (Revised by AV, 26-Oct-2022)

		Ref	Expression
	Assertion	wwlksnred	$⊢ N \in ℕ_{0} \to (W \in ((N + 1) WWalksN G) \to W prefix (N + 1) \in (N WWalksN G))$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
2		iswwlksn	$⊢ N + 1 \in ℕ_{0} \to (W \in ((N + 1) WWalksN G) \leftrightarrow (W \in WWalks (G) \land \|W\| = N + 1 + 1))$
3	1 2	syl	$⊢ N \in ℕ_{0} \to (W \in ((N + 1) WWalksN G) \leftrightarrow (W \in WWalks (G) \land \|W\| = N + 1 + 1))$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5		eqid	$⊢ Edg (G) = Edg (G)$
6	4 5	iswwlks	$⊢ W \in WWalks (G) \leftrightarrow (W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G))$
7		simp1	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to W \in Word Vtx (G)$
8		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
9	8	3ad2ant3	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to N + 1 \in ℕ$
10	1	nn0red	$⊢ N \in ℕ_{0} \to N + 1 \in ℝ$
11	10	lep1d	$⊢ N \in ℕ_{0} \to N + 1 \leq N + 1 + 1$
12	11	3ad2ant3	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to N + 1 \leq N + 1 + 1$
13		breq2	$⊢ \|W\| = N + 1 + 1 \to (N + 1 \leq \|W\| \leftrightarrow N + 1 \leq N + 1 + 1)$
14	13	3ad2ant2	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to (N + 1 \leq \|W\| \leftrightarrow N + 1 \leq N + 1 + 1)$
15	12 14	mpbird	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to N + 1 \leq \|W\|$
16		pfxn0	$⊢ (W \in Word Vtx (G) \land N + 1 \in ℕ \land N + 1 \leq \|W\|) \to W prefix (N + 1) \neq \emptyset$
17	7 9 15 16	syl3anc	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to W prefix (N + 1) \neq \emptyset$
18	17	3exp	$⊢ W \in Word Vtx (G) \to (\|W\| = N + 1 + 1 \to (N \in ℕ_{0} \to W prefix (N + 1) \neq \emptyset))$
19	18	3ad2ant2	$⊢ (W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to (\|W\| = N + 1 + 1 \to (N \in ℕ_{0} \to W prefix (N + 1) \neq \emptyset))$
20	19	imp	$⊢ ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1) \to (N \in ℕ_{0} \to W prefix (N + 1) \neq \emptyset)$
21	20	impcom	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to W prefix (N + 1) \neq \emptyset$
22		pfxcl	$⊢ W \in Word Vtx (G) \to W prefix (N + 1) \in Word Vtx (G)$
23	22	3ad2ant2	$⊢ (W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to W prefix (N + 1) \in Word Vtx (G)$
24	23	adantr	$⊢ ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1) \to W prefix (N + 1) \in Word Vtx (G)$
25	24	adantl	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to W prefix (N + 1) \in Word Vtx (G)$
26		oveq1	$⊢ \|W\| = N + 1 + 1 \to \|W\| - 1 = (N + 1) + 1 - 1$
27	1	nn0cnd	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
28		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
29	27 28	pncand	$⊢ N \in ℕ_{0} \to (N + 1) + 1 - 1 = N + 1$
30	26 29	sylan9eq	$⊢ (\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to \|W\| - 1 = N + 1$
31	30	oveq2d	$⊢ (\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to (0 ..^\|W\| - 1) = (0 ..^N + 1)$
32	31	raleqdv	$⊢ (\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to (\forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in Edg (G))$
33	32	adantl	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (\forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in Edg (G))$
34		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
35		nn0z	$⊢ N + 1 \in ℕ_{0} \to N + 1 \in ℤ$
36	1 35	syl	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ$
37		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
38	37	lep1d	$⊢ N \in ℕ_{0} \to N \leq N + 1$
39	34 36 38	3jca	$⊢ N \in ℕ_{0} \to (N \in ℤ \land N + 1 \in ℤ \land N \leq N + 1)$
40	39	ad2antll	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (N \in ℤ \land N + 1 \in ℤ \land N \leq N + 1)$
41		eluz2	$⊢ N + 1 \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land N + 1 \in ℤ \land N \leq N + 1)$
42	40 41	sylibr	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to N + 1 \in ℤ_{\geq N}$
43		fzoss2	$⊢ N + 1 \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^N + 1)$
44	42 43	syl	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (0 ..^N) \subseteq (0 ..^N + 1)$
45		ssralv	$⊢ (0 ..^N) \subseteq (0 ..^N + 1) \to (\forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in Edg (G))$
46	44 45	syl	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (\forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in Edg (G))$
47		simpll	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to W \in Word Vtx (G)$
48		nn0fz0	$⊢ N + 1 \in ℕ_{0} \leftrightarrow N + 1 \in (0 \dots N + 1)$
49	1 48	sylib	$⊢ N \in ℕ_{0} \to N + 1 \in (0 \dots N + 1)$
50	49	ad2antll	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to N + 1 \in (0 \dots N + 1)$
51		fzelp1	$⊢ N + 1 \in (0 \dots N + 1) \to N + 1 \in (0 \dots N + 1 + 1)$
52	50 51	syl	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to N + 1 \in (0 \dots N + 1 + 1)$
53		oveq2	$⊢ \|W\| = N + 1 + 1 \to (0 \dots \|W\|) = (0 \dots N + 1 + 1)$
54	53	eleq2d	$⊢ \|W\| = N + 1 + 1 \to (N + 1 \in (0 \dots \|W\|) \leftrightarrow N + 1 \in (0 \dots N + 1 + 1))$
55	54	adantr	$⊢ (\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to (N + 1 \in (0 \dots \|W\|) \leftrightarrow N + 1 \in (0 \dots N + 1 + 1))$
56	55	adantl	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (N + 1 \in (0 \dots \|W\|) \leftrightarrow N + 1 \in (0 \dots N + 1 + 1))$
57	52 56	mpbird	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to N + 1 \in (0 \dots \|W\|)$
58	57	adantr	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to N + 1 \in (0 \dots \|W\|)$
59		fzossfzop1	$⊢ N \in ℕ_{0} \to (0 ..^N) \subseteq (0 ..^N + 1)$
60	59	sseld	$⊢ N \in ℕ_{0} \to (i \in (0 ..^N) \to i \in (0 ..^N + 1))$
61	60	ad2antll	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (i \in (0 ..^N) \to i \in (0 ..^N + 1))$
62	61	imp	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to i \in (0 ..^N + 1)$
63		pfxfv	$⊢ (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|) \land i \in (0 ..^N + 1)) \to (W prefix (N + 1)) (i) = W (i)$
64	47 58 62 63	syl3anc	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (W prefix (N + 1)) (i) = W (i)$
65	64	eqcomd	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to W (i) = (W prefix (N + 1)) (i)$
66		fzofzp1	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots N)$
67	66	adantl	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to i + 1 \in (0 \dots N)$
68		fzval3	$⊢ N \in ℤ \to (0 \dots N) = (0 ..^N + 1)$
69	68	eqcomd	$⊢ N \in ℤ \to (0 ..^N + 1) = (0 \dots N)$
70	34 69	syl	$⊢ N \in ℕ_{0} \to (0 ..^N + 1) = (0 \dots N)$
71	70	eleq2d	$⊢ N \in ℕ_{0} \to (i + 1 \in (0 ..^N + 1) \leftrightarrow i + 1 \in (0 \dots N))$
72	71	ad2antll	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (i + 1 \in (0 ..^N + 1) \leftrightarrow i + 1 \in (0 \dots N))$
73	72	adantr	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (i + 1 \in (0 ..^N + 1) \leftrightarrow i + 1 \in (0 \dots N))$
74	67 73	mpbird	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to i + 1 \in (0 ..^N + 1)$
75		pfxfv	$⊢ (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|) \land i + 1 \in (0 ..^N + 1)) \to (W prefix (N + 1)) (i + 1) = W (i + 1)$
76	47 58 74 75	syl3anc	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (W prefix (N + 1)) (i + 1) = W (i + 1)$
77	76	eqcomd	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to W (i + 1) = (W prefix (N + 1)) (i + 1)$
78	65 77	preq12d	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to \{W (i), W (i + 1)\} = \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\}$
79	78	eleq1d	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (\{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
80	79	biimpd	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (\{W (i), W (i + 1)\} \in Edg (G) \to \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
81	80	ralimdva	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (\forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
82	46 81	syld	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (\forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
83	33 82	sylbid	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (\forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
84	83	imp	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to \forall i \in (0 ..^N) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G)$
85		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
86	85 28	pncand	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
87	86	oveq2d	$⊢ N \in ℕ_{0} \to (0 ..^N + 1 - 1) = (0 ..^N)$
88	87	ad2antll	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (0 ..^N + 1 - 1) = (0 ..^N)$
89	88	adantr	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to (0 ..^N + 1 - 1) = (0 ..^N)$
90	89	raleqdv	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to (\forall i \in (0 ..^N + 1 - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
91	84 90	mpbird	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to \forall i \in (0 ..^N + 1 - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G)$
92		pfxlen	$⊢ (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|)) \to \|W prefix (N + 1)\| = N + 1$
93	57 92	syldan	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to \|W prefix (N + 1)\| = N + 1$
94	93	oveq1d	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to \|W prefix (N + 1)\| - 1 = N + 1 - 1$
95	94	oveq2d	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (0 ..^\|W prefix (N + 1)\| - 1) = (0 ..^N + 1 - 1)$
96	95	raleqdv	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (\forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N + 1 - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
97	96	adantr	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to (\forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N + 1 - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
98	91 97	mpbird	$⊢ ((W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G)$
99	98	exp31	$⊢ W \in Word Vtx (G) \to ((\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to (\forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G)))$
100	99	com23	$⊢ W \in Word Vtx (G) \to (\forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \to ((\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G)))$
101	100	imp	$⊢ (W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to ((\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
102	101	3adant1	$⊢ (W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to ((\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
103	102	expdimp	$⊢ ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1) \to (N \in ℕ_{0} \to \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
104	103	impcom	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G)$
105	4 5	iswwlks	$⊢ W prefix (N + 1) \in WWalks (G) \leftrightarrow (W prefix (N + 1) \neq \emptyset \land W prefix (N + 1) \in Word Vtx (G) \land \forall i \in (0 ..^\|W prefix (N + 1)\| - 1) \{(W prefix (N + 1)) (i), (W prefix (N + 1)) (i + 1)\} \in Edg (G))$
106	21 25 104 105	syl3anbrc	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to W prefix (N + 1) \in WWalks (G)$
107		peano2nn0	$⊢ N + 1 \in ℕ_{0} \to N + 1 + 1 \in ℕ_{0}$
108	1 107	syl	$⊢ N \in ℕ_{0} \to N + 1 + 1 \in ℕ_{0}$
109		elfz2nn0	$⊢ N + 1 \in (0 \dots N + 1 + 1) \leftrightarrow (N + 1 \in ℕ_{0} \land N + 1 + 1 \in ℕ_{0} \land N + 1 \leq N + 1 + 1)$
110	1 108 11 109	syl3anbrc	$⊢ N \in ℕ_{0} \to N + 1 \in (0 \dots N + 1 + 1)$
111	110	adantl	$⊢ (\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to N + 1 \in (0 \dots N + 1 + 1)$
112	111 55	mpbird	$⊢ (\|W\| = N + 1 + 1 \land N \in ℕ_{0}) \to N + 1 \in (0 \dots \|W\|)$
113	112	anim2i	$⊢ (W \in Word Vtx (G) \land (\|W\| = N + 1 + 1 \land N \in ℕ_{0})) \to (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|))$
114	113	exp32	$⊢ W \in Word Vtx (G) \to (\|W\| = N + 1 + 1 \to (N \in ℕ_{0} \to (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|))))$
115	114	3ad2ant2	$⊢ (W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \to (\|W\| = N + 1 + 1 \to (N \in ℕ_{0} \to (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|))))$
116	115	imp	$⊢ ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1) \to (N \in ℕ_{0} \to (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|)))$
117	116	impcom	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to (W \in Word Vtx (G) \land N + 1 \in (0 \dots \|W\|))$
118	117 92	syl	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to \|W prefix (N + 1)\| = N + 1$
119		iswwlksn	$⊢ N \in ℕ_{0} \to (W prefix (N + 1) \in (N WWalksN G) \leftrightarrow (W prefix (N + 1) \in WWalks (G) \land \|W prefix (N + 1)\| = N + 1))$
120	119	adantr	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to (W prefix (N + 1) \in (N WWalksN G) \leftrightarrow (W prefix (N + 1) \in WWalks (G) \land \|W prefix (N + 1)\| = N + 1))$
121	106 118 120	mpbir2and	$⊢ (N \in ℕ_{0} \land ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1)) \to W prefix (N + 1) \in (N WWalksN G)$
122	121	expcom	$⊢ ((W \neq \emptyset \land W \in Word Vtx (G) \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G)) \land \|W\| = N + 1 + 1) \to (N \in ℕ_{0} \to W prefix (N + 1) \in (N WWalksN G))$
123	6 122	sylanb	$⊢ (W \in WWalks (G) \land \|W\| = N + 1 + 1) \to (N \in ℕ_{0} \to W prefix (N + 1) \in (N WWalksN G))$
124	123	com12	$⊢ N \in ℕ_{0} \to ((W \in WWalks (G) \land \|W\| = N + 1 + 1) \to W prefix (N + 1) \in (N WWalksN G))$
125	3 124	sylbid	$⊢ N \in ℕ_{0} \to (W \in ((N + 1) WWalksN G) \to W prefix (N + 1) \in (N WWalksN G))$

Metamath Proof Explorer

Theorem wwlksnred

Proof