wwlksubclwwlk

Description: Any prefix of a word representing a closed walk represents a walk. (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 28-Apr-2021) (Revised by AV, 1-Nov-2022)

		Ref	Expression
	Assertion	wwlksubclwwlk	$⊢ (M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to (X \in (N ClWWalksN G) \to X prefix M \in ((M - 1) WWalksN G))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ Edg (G) = Edg (G)$
3	1 2	clwwlknp	$⊢ X \in (N ClWWalksN G) \to ((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G) \land \{lastS (X), X (0)\} \in Edg (G))$
4		pfxcl	$⊢ X \in Word Vtx (G) \to X prefix M \in Word Vtx (G)$
5	4	adantr	$⊢ (X \in Word Vtx (G) \land \|X\| = N) \to X prefix M \in Word Vtx (G)$
6	5	ad2antrr	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to X prefix M \in Word Vtx (G)$
7		nnz	$⊢ M \in ℕ \to M \in ℤ$
8		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
9	8	ex	$⊢ M \in ℤ \to (N \in ℤ_{\geq (M + 1)} \to N - 1 \in ℤ_{\geq M})$
10	7 9	syl	$⊢ M \in ℕ \to (N \in ℤ_{\geq (M + 1)} \to N - 1 \in ℤ_{\geq M})$
11		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
12	7 11	syl	$⊢ M \in ℕ \to M - 1 \in ℤ$
13		nnre	$⊢ M \in ℕ \to M \in ℝ$
14	13	lem1d	$⊢ M \in ℕ \to M - 1 \leq M$
15		eluzuzle	$⊢ (M - 1 \in ℤ \land M - 1 \leq M) \to (N - 1 \in ℤ_{\geq M} \to N - 1 \in ℤ_{\geq (M - 1)})$
16	12 14 15	syl2anc	$⊢ M \in ℕ \to (N - 1 \in ℤ_{\geq M} \to N - 1 \in ℤ_{\geq (M - 1)})$
17	10 16	syld	$⊢ M \in ℕ \to (N \in ℤ_{\geq (M + 1)} \to N - 1 \in ℤ_{\geq (M - 1)})$
18	17	imp	$⊢ (M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq (M - 1)}$
19		fzoss2	$⊢ N - 1 \in ℤ_{\geq (M - 1)} \to (0 ..^M - 1) \subseteq (0 ..^N - 1)$
20	18 19	syl	$⊢ (M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to (0 ..^M - 1) \subseteq (0 ..^N - 1)$
21	20	adantl	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (0 ..^M - 1) \subseteq (0 ..^N - 1)$
22		ssralv	$⊢ (0 ..^M - 1) \subseteq (0 ..^N - 1) \to (\forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^M - 1) \{X (i), X (i + 1)\} \in Edg (G))$
23	21 22	syl	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (\forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^M - 1) \{X (i), X (i + 1)\} \in Edg (G))$
24		simpll	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to X \in Word Vtx (G)$
25	24	adantr	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to X \in Word Vtx (G)$
26		eluz2	$⊢ N \in ℤ_{\geq (M + 1)} \leftrightarrow (M + 1 \in ℤ \land N \in ℤ \land M + 1 \leq N)$
27	13	adantr	$⊢ (M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \to M \in ℝ$
28		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
29	13 28	syl	$⊢ M \in ℕ \to M + 1 \in ℝ$
30	29	adantr	$⊢ (M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \to M + 1 \in ℝ$
31		zre	$⊢ N \in ℤ \to N \in ℝ$
32	31	ad2antrl	$⊢ (M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \to N \in ℝ$
33	13	lep1d	$⊢ M \in ℕ \to M \leq M + 1$
34	33	adantr	$⊢ (M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \to M \leq M + 1$
35		simpr	$⊢ (N \in ℤ \land M + 1 \leq N) \to M + 1 \leq N$
36	35	adantl	$⊢ (M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \to M + 1 \leq N$
37	27 30 32 34 36	letrd	$⊢ (M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \to M \leq N$
38		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
39	38	ad2antrr	$⊢ ((M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \land M \leq N) \to M \in ℕ_{0}$
40		simpr	$⊢ (M \in ℕ \land N \in ℤ) \to N \in ℤ$
41	40	adantr	$⊢ ((M \in ℕ \land N \in ℤ) \land M \leq N) \to N \in ℤ$
42		0red	$⊢ (M \in ℕ \land N \in ℤ) \to 0 \in ℝ$
43	13	adantr	$⊢ (M \in ℕ \land N \in ℤ) \to M \in ℝ$
44	31	adantl	$⊢ (M \in ℕ \land N \in ℤ) \to N \in ℝ$
45	42 43 44	3jca	$⊢ (M \in ℕ \land N \in ℤ) \to (0 \in ℝ \land M \in ℝ \land N \in ℝ)$
46	45	adantr	$⊢ ((M \in ℕ \land N \in ℤ) \land M \leq N) \to (0 \in ℝ \land M \in ℝ \land N \in ℝ)$
47	38	nn0ge0d	$⊢ M \in ℕ \to 0 \leq M$
48	47	adantr	$⊢ (M \in ℕ \land N \in ℤ) \to 0 \leq M$
49	48	anim1i	$⊢ ((M \in ℕ \land N \in ℤ) \land M \leq N) \to (0 \leq M \land M \leq N)$
50		letr	$⊢ (0 \in ℝ \land M \in ℝ \land N \in ℝ) \to ((0 \leq M \land M \leq N) \to 0 \leq N)$
51	46 49 50	sylc	$⊢ ((M \in ℕ \land N \in ℤ) \land M \leq N) \to 0 \leq N$
52		elnn0z	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℤ \land 0 \leq N)$
53	41 51 52	sylanbrc	$⊢ ((M \in ℕ \land N \in ℤ) \land M \leq N) \to N \in ℕ_{0}$
54	53	adantlrr	$⊢ ((M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \land M \leq N) \to N \in ℕ_{0}$
55		simpr	$⊢ ((M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \land M \leq N) \to M \leq N$
56	39 54 55	3jca	$⊢ ((M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \land M \leq N) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
57	37 56	mpdan	$⊢ (M \in ℕ \land (N \in ℤ \land M + 1 \leq N)) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
58	57	expcom	$⊢ (N \in ℤ \land M + 1 \leq N) \to (M \in ℕ \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
59	58	3adant1	$⊢ (M + 1 \in ℤ \land N \in ℤ \land M + 1 \leq N) \to (M \in ℕ \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
60	26 59	sylbi	$⊢ N \in ℤ_{\geq (M + 1)} \to (M \in ℕ \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
61	60	impcom	$⊢ (M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
62		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
63	61 62	sylibr	$⊢ (M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to M \in (0 \dots N)$
64	63	adantl	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to M \in (0 \dots N)$
65		oveq2	$⊢ \|X\| = N \to (0 \dots \|X\|) = (0 \dots N)$
66	65	eleq2d	$⊢ \|X\| = N \to (M \in (0 \dots \|X\|) \leftrightarrow M \in (0 \dots N))$
67	66	adantl	$⊢ (X \in Word Vtx (G) \land \|X\| = N) \to (M \in (0 \dots \|X\|) \leftrightarrow M \in (0 \dots N))$
68	67	adantr	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (M \in (0 \dots \|X\|) \leftrightarrow M \in (0 \dots N))$
69	64 68	mpbird	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to M \in (0 \dots \|X\|)$
70	69	adantr	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to M \in (0 \dots \|X\|)$
71		eluz2	$⊢ M \in ℤ_{\geq (M - 1)} \leftrightarrow (M - 1 \in ℤ \land M \in ℤ \land M - 1 \leq M)$
72	12 7 14 71	syl3anbrc	$⊢ M \in ℕ \to M \in ℤ_{\geq (M - 1)}$
73		fzoss2	$⊢ M \in ℤ_{\geq (M - 1)} \to (0 ..^M - 1) \subseteq (0 ..^M)$
74	72 73	syl	$⊢ M \in ℕ \to (0 ..^M - 1) \subseteq (0 ..^M)$
75	74	sseld	$⊢ M \in ℕ \to (i \in (0 ..^M - 1) \to i \in (0 ..^M))$
76	75	ad2antrl	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (i \in (0 ..^M - 1) \to i \in (0 ..^M))$
77	76	imp	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to i \in (0 ..^M)$
78		pfxfv	$⊢ (X \in Word Vtx (G) \land M \in (0 \dots \|X\|) \land i \in (0 ..^M)) \to (X prefix M) (i) = X (i)$
79	25 70 77 78	syl3anc	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to (X prefix M) (i) = X (i)$
80	79	eqcomd	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to X (i) = (X prefix M) (i)$
81		fzonn0p1p1	$⊢ i \in (0 ..^M - 1) \to i + 1 \in (0 ..^M - 1 + 1)$
82		nncn	$⊢ M \in ℕ \to M \in ℂ$
83		npcan1	$⊢ M \in ℂ \to M - 1 + 1 = M$
84	82 83	syl	$⊢ M \in ℕ \to M - 1 + 1 = M$
85	84	oveq2d	$⊢ M \in ℕ \to (0 ..^M - 1 + 1) = (0 ..^M)$
86	85	eleq2d	$⊢ M \in ℕ \to (i + 1 \in (0 ..^M - 1 + 1) \leftrightarrow i + 1 \in (0 ..^M))$
87	81 86	syl5ib	$⊢ M \in ℕ \to (i \in (0 ..^M - 1) \to i + 1 \in (0 ..^M))$
88	87	ad2antrl	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (i \in (0 ..^M - 1) \to i + 1 \in (0 ..^M))$
89	88	imp	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to i + 1 \in (0 ..^M)$
90		pfxfv	$⊢ (X \in Word Vtx (G) \land M \in (0 \dots \|X\|) \land i + 1 \in (0 ..^M)) \to (X prefix M) (i + 1) = X (i + 1)$
91	25 70 89 90	syl3anc	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to (X prefix M) (i + 1) = X (i + 1)$
92	91	eqcomd	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to X (i + 1) = (X prefix M) (i + 1)$
93	80 92	preq12d	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to \{X (i), X (i + 1)\} = \{(X prefix M) (i), (X prefix M) (i + 1)\}$
94	93	eleq1d	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \land i \in (0 ..^M - 1)) \to (\{X (i), X (i + 1)\} \in Edg (G) \leftrightarrow \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G))$
95	94	ralbidva	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (\forall i \in (0 ..^M - 1) \{X (i), X (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^M - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G))$
96	23 95	sylibd	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (\forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^M - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G))$
97	96	impancom	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \to ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to \forall i \in (0 ..^M - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G))$
98	97	imp	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to \forall i \in (0 ..^M - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G)$
99	24 69	jca	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (X \in Word Vtx (G) \land M \in (0 \dots \|X\|))$
100	99	adantlr	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (X \in Word Vtx (G) \land M \in (0 \dots \|X\|))$
101		pfxlen	$⊢ (X \in Word Vtx (G) \land M \in (0 \dots \|X\|)) \to \|X prefix M\| = M$
102	100 101	syl	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to \|X prefix M\| = M$
103	102	oveq1d	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to \|X prefix M\| - 1 = M - 1$
104	103	oveq2d	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (0 ..^\|X prefix M\| - 1) = (0 ..^M - 1)$
105	104	raleqdv	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (\forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^M - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G))$
106	98 105	mpbird	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G)$
107	24 69 101	syl2anc	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to \|X prefix M\| = M$
108	84	eqcomd	$⊢ M \in ℕ \to M = M - 1 + 1$
109	108	ad2antrl	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to M = M - 1 + 1$
110	107 109	eqtrd	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to \|X prefix M\| = M - 1 + 1$
111	110	adantlr	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to \|X prefix M\| = M - 1 + 1$
112	6 106 111	3jca	$⊢ (((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \land (M \in ℕ \land N \in ℤ_{\geq (M + 1)})) \to (X prefix M \in Word Vtx (G) \land \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \land \|X prefix M\| = M - 1 + 1)$
113	112	ex	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G)) \to ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to (X prefix M \in Word Vtx (G) \land \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \land \|X prefix M\| = M - 1 + 1))$
114	113	3adant3	$⊢ ((X \in Word Vtx (G) \land \|X\| = N) \land \forall i \in (0 ..^N - 1) \{X (i), X (i + 1)\} \in Edg (G) \land \{lastS (X), X (0)\} \in Edg (G)) \to ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to (X prefix M \in Word Vtx (G) \land \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \land \|X prefix M\| = M - 1 + 1))$
115	3 114	syl	$⊢ X \in (N ClWWalksN G) \to ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to (X prefix M \in Word Vtx (G) \land \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \land \|X prefix M\| = M - 1 + 1))$
116	115	impcom	$⊢ ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \land X \in (N ClWWalksN G)) \to (X prefix M \in Word Vtx (G) \land \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \land \|X prefix M\| = M - 1 + 1)$
117		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
118	117	ad2antrr	$⊢ ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \land X \in (N ClWWalksN G)) \to M - 1 \in ℕ_{0}$
119	1 2	iswwlksnx	$⊢ M - 1 \in ℕ_{0} \to (X prefix M \in ((M - 1) WWalksN G) \leftrightarrow (X prefix M \in Word Vtx (G) \land \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \land \|X prefix M\| = M - 1 + 1))$
120	118 119	syl	$⊢ ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \land X \in (N ClWWalksN G)) \to (X prefix M \in ((M - 1) WWalksN G) \leftrightarrow (X prefix M \in Word Vtx (G) \land \forall i \in (0 ..^\|X prefix M\| - 1) \{(X prefix M) (i), (X prefix M) (i + 1)\} \in Edg (G) \land \|X prefix M\| = M - 1 + 1))$
121	116 120	mpbird	$⊢ ((M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \land X \in (N ClWWalksN G)) \to X prefix M \in ((M - 1) WWalksN G)$
122	121	ex	$⊢ (M \in ℕ \land N \in ℤ_{\geq (M + 1)}) \to (X \in (N ClWWalksN G) \to X prefix M \in ((M - 1) WWalksN G))$

Metamath Proof Explorer

Theorem wwlksubclwwlk

Proof