clwwlkf

Description: Lemma 1 for clwwlkf1o : F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
	clwwlkf1o.f	$⊢ F = (t \in D ⟼ t prefix N)$
Assertion	clwwlkf	$⊢ N \in ℕ \to F : D ⟶ N ClWWalksN G$

Proof

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
2		clwwlkf1o.f	$⊢ F = (t \in D ⟼ t prefix N)$
3		fveq2	$⊢ w = t \to lastS (w) = lastS (t)$
4		fveq1	$⊢ w = t \to w (0) = t (0)$
5	3 4	eqeq12d	$⊢ w = t \to (lastS (w) = w (0) \leftrightarrow lastS (t) = t (0))$
6	5 1	elrab2	$⊢ t \in D \leftrightarrow (t \in (N WWalksN G) \land lastS (t) = t (0))$
7		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
8		iswwlksn	$⊢ N \in ℕ_{0} \to (t \in (N WWalksN G) \leftrightarrow (t \in WWalks (G) \land \|t\| = N + 1))$
9	7 8	syl	$⊢ N \in ℕ \to (t \in (N WWalksN G) \leftrightarrow (t \in WWalks (G) \land \|t\| = N + 1))$
10		eqid	$⊢ Vtx (G) = Vtx (G)$
11		eqid	$⊢ Edg (G) = Edg (G)$
12	10 11	iswwlks	$⊢ t \in WWalks (G) \leftrightarrow (t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G))$
13	12	a1i	$⊢ N \in ℕ \to (t \in WWalks (G) \leftrightarrow (t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)))$
14	13	anbi1d	$⊢ N \in ℕ \to ((t \in WWalks (G) \land \|t\| = N + 1) \leftrightarrow ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1))$
15	9 14	bitrd	$⊢ N \in ℕ \to (t \in (N WWalksN G) \leftrightarrow ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1))$
16		simpll	$⊢ ((t \in Word Vtx (G) \land \|t\| = N + 1) \land N \in ℕ) \to t \in Word Vtx (G)$
17		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
18	7 17	syl	$⊢ N \in ℕ \to N + 1 \in ℕ_{0}$
19		nnre	$⊢ N \in ℕ \to N \in ℝ$
20	19	lep1d	$⊢ N \in ℕ \to N \leq N + 1$
21		elfz2nn0	$⊢ N \in (0 \dots N + 1) \leftrightarrow (N \in ℕ_{0} \land N + 1 \in ℕ_{0} \land N \leq N + 1)$
22	7 18 20 21	syl3anbrc	$⊢ N \in ℕ \to N \in (0 \dots N + 1)$
23	22	adantl	$⊢ ((t \in Word Vtx (G) \land \|t\| = N + 1) \land N \in ℕ) \to N \in (0 \dots N + 1)$
24		oveq2	$⊢ \|t\| = N + 1 \to (0 \dots \|t\|) = (0 \dots N + 1)$
25	24	eleq2d	$⊢ \|t\| = N + 1 \to (N \in (0 \dots \|t\|) \leftrightarrow N \in (0 \dots N + 1))$
26	25	adantl	$⊢ (t \in Word Vtx (G) \land \|t\| = N + 1) \to (N \in (0 \dots \|t\|) \leftrightarrow N \in (0 \dots N + 1))$
27	26	adantr	$⊢ ((t \in Word Vtx (G) \land \|t\| = N + 1) \land N \in ℕ) \to (N \in (0 \dots \|t\|) \leftrightarrow N \in (0 \dots N + 1))$
28	23 27	mpbird	$⊢ ((t \in Word Vtx (G) \land \|t\| = N + 1) \land N \in ℕ) \to N \in (0 \dots \|t\|)$
29	16 28	jca	$⊢ ((t \in Word Vtx (G) \land \|t\| = N + 1) \land N \in ℕ) \to (t \in Word Vtx (G) \land N \in (0 \dots \|t\|))$
30		pfxlen	$⊢ (t \in Word Vtx (G) \land N \in (0 \dots \|t\|)) \to \|t prefix N\| = N$
31	29 30	syl	$⊢ ((t \in Word Vtx (G) \land \|t\| = N + 1) \land N \in ℕ) \to \|t prefix N\| = N$
32	31	ex	$⊢ (t \in Word Vtx (G) \land \|t\| = N + 1) \to (N \in ℕ \to \|t prefix N\| = N)$
33	32	3ad2antl2	$⊢ ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1) \to (N \in ℕ \to \|t prefix N\| = N)$
34	33	impcom	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to \|t prefix N\| = N$
35	34	adantr	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to \|t prefix N\| = N$
36		pfxcl	$⊢ t \in Word Vtx (G) \to t prefix N \in Word Vtx (G)$
37	36	3ad2ant2	$⊢ (t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \to t prefix N \in Word Vtx (G)$
38	37	ad2antrl	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to t prefix N \in Word Vtx (G)$
39	38	ad2antrl	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to t prefix N \in Word Vtx (G)$
40		oveq1	$⊢ \|t\| = N + 1 \to \|t\| - 1 = N + 1 - 1$
41	40	oveq2d	$⊢ \|t\| = N + 1 \to (0 ..^\|t\| - 1) = (0 ..^N + 1 - 1)$
42		nncn	$⊢ N \in ℕ \to N \in ℂ$
43		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
44	42 43	pncand	$⊢ N \in ℕ \to N + 1 - 1 = N$
45	44	oveq2d	$⊢ N \in ℕ \to (0 ..^N + 1 - 1) = (0 ..^N)$
46	41 45	sylan9eqr	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (0 ..^\|t\| - 1) = (0 ..^N)$
47	46	raleqdv	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G))$
48		nnz	$⊢ N \in ℕ \to N \in ℤ$
49		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
50	48 49	syl	$⊢ N \in ℕ \to N - 1 \in ℤ$
51	19	lem1d	$⊢ N \in ℕ \to N - 1 \leq N$
52		eluz2	$⊢ N \in ℤ_{\geq (N - 1)} \leftrightarrow (N - 1 \in ℤ \land N \in ℤ \land N - 1 \leq N)$
53	50 48 51 52	syl3anbrc	$⊢ N \in ℕ \to N \in ℤ_{\geq (N - 1)}$
54		fzoss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (0 ..^N - 1) \subseteq (0 ..^N)$
55	53 54	syl	$⊢ N \in ℕ \to (0 ..^N - 1) \subseteq (0 ..^N)$
56	55	adantr	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (0 ..^N - 1) \subseteq (0 ..^N)$
57		ssralv	$⊢ (0 ..^N - 1) \subseteq (0 ..^N) \to (\forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N - 1) \{t (i), t (i + 1)\} \in Edg (G))$
58	56 57	syl	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (\forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N - 1) \{t (i), t (i + 1)\} \in Edg (G))$
59		simplr	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to t \in Word Vtx (G)$
60	22	adantr	$⊢ (N \in ℕ \land \|t\| = N + 1) \to N \in (0 \dots N + 1)$
61	25	adantl	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (N \in (0 \dots \|t\|) \leftrightarrow N \in (0 \dots N + 1))$
62	60 61	mpbird	$⊢ (N \in ℕ \land \|t\| = N + 1) \to N \in (0 \dots \|t\|)$
63	62	ad2antrr	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to N \in (0 \dots \|t\|)$
64	55	sseld	$⊢ N \in ℕ \to (i \in (0 ..^N - 1) \to i \in (0 ..^N))$
65	64	ad2antrr	$⊢ ((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \to (i \in (0 ..^N - 1) \to i \in (0 ..^N))$
66	65	imp	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to i \in (0 ..^N)$
67		pfxfv	$⊢ (t \in Word Vtx (G) \land N \in (0 \dots \|t\|) \land i \in (0 ..^N)) \to (t prefix N) (i) = t (i)$
68	67	eqcomd	$⊢ (t \in Word Vtx (G) \land N \in (0 \dots \|t\|) \land i \in (0 ..^N)) \to t (i) = (t prefix N) (i)$
69	59 63 66 68	syl3anc	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to t (i) = (t prefix N) (i)$
70	48	ad2antrr	$⊢ ((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \to N \in ℤ$
71		elfzom1elp1fzo	$⊢ (N \in ℤ \land i \in (0 ..^N - 1)) \to i + 1 \in (0 ..^N)$
72	70 71	sylan	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to i + 1 \in (0 ..^N)$
73		pfxfv	$⊢ (t \in Word Vtx (G) \land N \in (0 \dots \|t\|) \land i + 1 \in (0 ..^N)) \to (t prefix N) (i + 1) = t (i + 1)$
74	73	eqcomd	$⊢ (t \in Word Vtx (G) \land N \in (0 \dots \|t\|) \land i + 1 \in (0 ..^N)) \to t (i + 1) = (t prefix N) (i + 1)$
75	59 63 72 74	syl3anc	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to t (i + 1) = (t prefix N) (i + 1)$
76	69 75	preq12d	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to \{t (i), t (i + 1)\} = \{(t prefix N) (i), (t prefix N) (i + 1)\}$
77	76	eleq1d	$⊢ (((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \land i \in (0 ..^N - 1)) \to (\{t (i), t (i + 1)\} \in Edg (G) \leftrightarrow \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))$
78	77	ralbidva	$⊢ ((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \to (\forall i \in (0 ..^N - 1) \{t (i), t (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))$
79	78	biimpd	$⊢ ((N \in ℕ \land \|t\| = N + 1) \land t \in Word Vtx (G)) \to (\forall i \in (0 ..^N - 1) \{t (i), t (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))$
80	79	ex	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (t \in Word Vtx (G) \to (\forall i \in (0 ..^N - 1) \{t (i), t (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)))$
81	80	com23	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (\forall i \in (0 ..^N - 1) \{t (i), t (i + 1)\} \in Edg (G) \to (t \in Word Vtx (G) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)))$
82	58 81	syld	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (\forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G) \to (t \in Word Vtx (G) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)))$
83	47 82	sylbid	$⊢ (N \in ℕ \land \|t\| = N + 1) \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \to (t \in Word Vtx (G) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)))$
84	83	ex	$⊢ N \in ℕ \to (\|t\| = N + 1 \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \to (t \in Word Vtx (G) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))))$
85	84	com23	$⊢ N \in ℕ \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \to (\|t\| = N + 1 \to (t \in Word Vtx (G) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))))$
86	85	com14	$⊢ t \in Word Vtx (G) \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \to (\|t\| = N + 1 \to (N \in ℕ \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))))$
87	86	imp	$⊢ (t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \to (\|t\| = N + 1 \to (N \in ℕ \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)))$
88	87	3adant1	$⊢ (t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \to (\|t\| = N + 1 \to (N \in ℕ \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)))$
89	88	imp	$⊢ ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1) \to (N \in ℕ \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))$
90	89	impcom	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)$
91	90	ad2antrl	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)$
92		oveq1	$⊢ \|t prefix N\| = N \to \|t prefix N\| - 1 = N - 1$
93	92	oveq2d	$⊢ \|t prefix N\| = N \to (0 ..^\|t prefix N\| - 1) = (0 ..^N - 1)$
94	93	adantr	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to (0 ..^\|t prefix N\| - 1) = (0 ..^N - 1)$
95	94	raleqdv	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to (\forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G))$
96	91 95	mpbird	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G)$
97		simprl2	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to t \in Word Vtx (G)$
98	20	ancli	$⊢ N \in ℕ \to (N \in ℕ \land N \leq N + 1)$
99	48	peano2zd	$⊢ N \in ℕ \to N + 1 \in ℤ$
100		fznn	$⊢ N + 1 \in ℤ \to (N \in (1 \dots N + 1) \leftrightarrow (N \in ℕ \land N \leq N + 1))$
101	99 100	syl	$⊢ N \in ℕ \to (N \in (1 \dots N + 1) \leftrightarrow (N \in ℕ \land N \leq N + 1))$
102	98 101	mpbird	$⊢ N \in ℕ \to N \in (1 \dots N + 1)$
103	102	adantr	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to N \in (1 \dots N + 1)$
104		oveq2	$⊢ \|t\| = N + 1 \to (1 \dots \|t\|) = (1 \dots N + 1)$
105	104	eleq2d	$⊢ \|t\| = N + 1 \to (N \in (1 \dots \|t\|) \leftrightarrow N \in (1 \dots N + 1))$
106	105	adantl	$⊢ ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1) \to (N \in (1 \dots \|t\|) \leftrightarrow N \in (1 \dots N + 1))$
107	106	adantl	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to (N \in (1 \dots \|t\|) \leftrightarrow N \in (1 \dots N + 1))$
108	103 107	mpbird	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to N \in (1 \dots \|t\|)$
109	97 108	jca	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to (t \in Word Vtx (G) \land N \in (1 \dots \|t\|))$
110	109	adantr	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to (t \in Word Vtx (G) \land N \in (1 \dots \|t\|))$
111		pfxfvlsw	$⊢ (t \in Word Vtx (G) \land N \in (1 \dots \|t\|)) \to lastS (t prefix N) = t (N - 1)$
112	110 111	syl	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to lastS (t prefix N) = t (N - 1)$
113		pfxfv0	$⊢ (t \in Word Vtx (G) \land N \in (1 \dots \|t\|)) \to (t prefix N) (0) = t (0)$
114	109 113	syl	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to (t prefix N) (0) = t (0)$
115	114	adantr	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to (t prefix N) (0) = t (0)$
116	112 115	preq12d	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to \{lastS (t prefix N), (t prefix N) (0)\} = \{t (N - 1), t (0)\}$
117		eqcom	$⊢ lastS (t) = t (0) \leftrightarrow t (0) = lastS (t)$
118	117	bilani	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to t (0) = lastS (t)$
119		lsw	$⊢ t \in Word Vtx (G) \to lastS (t) = t (\|t\| - 1)$
120	119	3ad2ant2	$⊢ (t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \to lastS (t) = t (\|t\| - 1)$
121	120	ad2antrl	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to lastS (t) = t (\|t\| - 1)$
122	121	adantr	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to lastS (t) = t (\|t\| - 1)$
123	40	adantl	$⊢ ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1) \to \|t\| - 1 = N + 1 - 1$
124	123 44	sylan9eqr	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to \|t\| - 1 = N$
125	124	adantr	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to \|t\| - 1 = N$
126	125	fveq2d	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to t (\|t\| - 1) = t (N)$
127	118 122 126	3eqtrd	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to t (0) = t (N)$
128	127	preq2d	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to \{t (N - 1), t (0)\} = \{t (N - 1), t (N)\}$
129	40 44	sylan9eq	$⊢ (\|t\| = N + 1 \land N \in ℕ) \to \|t\| - 1 = N$
130	129	oveq2d	$⊢ (\|t\| = N + 1 \land N \in ℕ) \to (0 ..^\|t\| - 1) = (0 ..^N)$
131	130	raleqdv	$⊢ (\|t\| = N + 1 \land N \in ℕ) \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G))$
132		fzo0end	$⊢ N \in ℕ \to N - 1 \in (0 ..^N)$
133		fveq2	$⊢ i = N - 1 \to t (i) = t (N - 1)$
134		fvoveq1	$⊢ i = N - 1 \to t (i + 1) = t (N - 1 + 1)$
135	133 134	preq12d	$⊢ i = N - 1 \to \{t (i), t (i + 1)\} = \{t (N - 1), t (N - 1 + 1)\}$
136	135	eleq1d	$⊢ i = N - 1 \to (\{t (i), t (i + 1)\} \in Edg (G) \leftrightarrow \{t (N - 1), t (N - 1 + 1)\} \in Edg (G))$
137	136	rspcva	$⊢ (N - 1 \in (0 ..^N) \land \forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G)) \to \{t (N - 1), t (N - 1 + 1)\} \in Edg (G)$
138	132 137	sylan	$⊢ (N \in ℕ \land \forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G)) \to \{t (N - 1), t (N - 1 + 1)\} \in Edg (G)$
139	42 43	npcand	$⊢ N \in ℕ \to N - 1 + 1 = N$
140	139	fveq2d	$⊢ N \in ℕ \to t (N - 1 + 1) = t (N)$
141	140	preq2d	$⊢ N \in ℕ \to \{t (N - 1), t (N - 1 + 1)\} = \{t (N - 1), t (N)\}$
142	141	eleq1d	$⊢ N \in ℕ \to (\{t (N - 1), t (N - 1 + 1)\} \in Edg (G) \leftrightarrow \{t (N - 1), t (N)\} \in Edg (G))$
143	142	biimpd	$⊢ N \in ℕ \to (\{t (N - 1), t (N - 1 + 1)\} \in Edg (G) \to \{t (N - 1), t (N)\} \in Edg (G))$
144	143	adantr	$⊢ (N \in ℕ \land \forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G)) \to (\{t (N - 1), t (N - 1 + 1)\} \in Edg (G) \to \{t (N - 1), t (N)\} \in Edg (G))$
145	138 144	mpd	$⊢ (N \in ℕ \land \forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G)) \to \{t (N - 1), t (N)\} \in Edg (G)$
146	145	ex	$⊢ N \in ℕ \to (\forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G) \to \{t (N - 1), t (N)\} \in Edg (G))$
147	146	adantl	$⊢ (\|t\| = N + 1 \land N \in ℕ) \to (\forall i \in (0 ..^N) \{t (i), t (i + 1)\} \in Edg (G) \to \{t (N - 1), t (N)\} \in Edg (G))$
148	131 147	sylbid	$⊢ (\|t\| = N + 1 \land N \in ℕ) \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \to \{t (N - 1), t (N)\} \in Edg (G))$
149	148	ex	$⊢ \|t\| = N + 1 \to (N \in ℕ \to (\forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \to \{t (N - 1), t (N)\} \in Edg (G)))$
150	149	com3r	$⊢ \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G) \to (\|t\| = N + 1 \to (N \in ℕ \to \{t (N - 1), t (N)\} \in Edg (G)))$
151	150	3ad2ant3	$⊢ (t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \to (\|t\| = N + 1 \to (N \in ℕ \to \{t (N - 1), t (N)\} \in Edg (G)))$
152	151	imp	$⊢ ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1) \to (N \in ℕ \to \{t (N - 1), t (N)\} \in Edg (G))$
153	152	impcom	$⊢ (N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \to \{t (N - 1), t (N)\} \in Edg (G)$
154	153	adantr	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to \{t (N - 1), t (N)\} \in Edg (G)$
155	128 154	eqeltrd	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to \{t (N - 1), t (0)\} \in Edg (G)$
156	116 155	eqeltrd	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)$
157	156	adantl	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)$
158	39 96 157	3jca	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to (t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G))$
159		simpl	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to \|t prefix N\| = N$
160	158 159	jca	$⊢ (\|t prefix N\| = N \land ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0))) \to ((t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)) \land \|t prefix N\| = N)$
161	35 160	mpancom	$⊢ ((N \in ℕ \land ((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1)) \land lastS (t) = t (0)) \to ((t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)) \land \|t prefix N\| = N)$
162	161	exp31	$⊢ N \in ℕ \to (((t \neq \emptyset \land t \in Word Vtx (G) \land \forall i \in (0 ..^\|t\| - 1) \{t (i), t (i + 1)\} \in Edg (G)) \land \|t\| = N + 1) \to (lastS (t) = t (0) \to ((t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)) \land \|t prefix N\| = N)))$
163	15 162	sylbid	$⊢ N \in ℕ \to (t \in (N WWalksN G) \to (lastS (t) = t (0) \to ((t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)) \land \|t prefix N\| = N)))$
164	163	imp32	$⊢ (N \in ℕ \land (t \in (N WWalksN G) \land lastS (t) = t (0))) \to ((t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)) \land \|t prefix N\| = N)$
165	10 11	isclwwlknx	$⊢ N \in ℕ \to (t prefix N \in (N ClWWalksN G) \leftrightarrow ((t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)) \land \|t prefix N\| = N))$
166	165	adantr	$⊢ (N \in ℕ \land (t \in (N WWalksN G) \land lastS (t) = t (0))) \to (t prefix N \in (N ClWWalksN G) \leftrightarrow ((t prefix N \in Word Vtx (G) \land \forall i \in (0 ..^\|t prefix N\| - 1) \{(t prefix N) (i), (t prefix N) (i + 1)\} \in Edg (G) \land \{lastS (t prefix N), (t prefix N) (0)\} \in Edg (G)) \land \|t prefix N\| = N))$
167	164 166	mpbird	$⊢ (N \in ℕ \land (t \in (N WWalksN G) \land lastS (t) = t (0))) \to t prefix N \in (N ClWWalksN G)$
168	6 167	sylan2b	$⊢ (N \in ℕ \land t \in D) \to t prefix N \in (N ClWWalksN G)$
169	168 2	fmptd	$⊢ N \in ℕ \to F : D ⟶ N ClWWalksN G$

Metamath Proof Explorer

Theorem clwwlkf

Proof