wwlksnext

Description: Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021)

	Ref	Expression
Hypotheses	wwlksnext.v	$⊢ V = Vtx (G)$
	wwlksnext.e	$⊢ E = Edg (G)$
Assertion	wwlksnext	$⊢ (T \in (N WWalksN G) \land S \in V \land \{lastS (T), S\} \in E) \to T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G)$

Proof

Step	Hyp	Ref	Expression
1		wwlksnext.v	$⊢ V = Vtx (G)$
2		wwlksnext.e	$⊢ E = Edg (G)$
3	1	wwlknbp	$⊢ T \in (N WWalksN G) \to (G \in V \land N \in ℕ_{0} \land T \in Word V)$
4	1 2	wwlknp	$⊢ T \in (N WWalksN G) \to (T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E)$
5		simp1	$⊢ (T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \to T \in Word V$
6		simprl	$⊢ (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to S \in V$
7		cats1un	$⊢ (T \in Word V \land S \in V) \to T ++ ⟨“ S ”⟩ = T \cup \{⟨\|T\|, S⟩\}$
8	5 6 7	syl2an	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to T ++ ⟨“ S ”⟩ = T \cup \{⟨\|T\|, S⟩\}$
9		opex	$⊢ ⟨\|T\|, S⟩ \in V$
10	9	snnz	$⊢ \{⟨\|T\|, S⟩\} \neq \emptyset$
11	10	neii	$⊢ \neg \{⟨\|T\|, S⟩\} = \emptyset$
12	11	intnan	$⊢ \neg (T = \emptyset \land \{⟨\|T\|, S⟩\} = \emptyset)$
13		df-ne	$⊢ T \cup \{⟨\|T\|, S⟩\} \neq \emptyset \leftrightarrow \neg T \cup \{⟨\|T\|, S⟩\} = \emptyset$
14		un00	$⊢ (T = \emptyset \land \{⟨\|T\|, S⟩\} = \emptyset) \leftrightarrow T \cup \{⟨\|T\|, S⟩\} = \emptyset$
15	13 14	xchbinxr	$⊢ T \cup \{⟨\|T\|, S⟩\} \neq \emptyset \leftrightarrow \neg (T = \emptyset \land \{⟨\|T\|, S⟩\} = \emptyset)$
16	12 15	mpbir	$⊢ T \cup \{⟨\|T\|, S⟩\} \neq \emptyset$
17	16	a1i	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to T \cup \{⟨\|T\|, S⟩\} \neq \emptyset$
18	8 17	eqnetrd	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to T ++ ⟨“ S ”⟩ \neq \emptyset$
19		s1cl	$⊢ S \in V \to ⟨“ S ”⟩ \in Word V$
20	19	ad2antrl	$⊢ (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to ⟨“ S ”⟩ \in Word V$
21		ccatcl	$⊢ (T \in Word V \land ⟨“ S ”⟩ \in Word V) \to T ++ ⟨“ S ”⟩ \in Word V$
22	5 20 21	syl2an	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to T ++ ⟨“ S ”⟩ \in Word V$
23		simplrl	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to T \in Word V$
24		fzossfzop1	$⊢ N \in ℕ_{0} \to (0 ..^N) \subseteq (0 ..^N + 1)$
25	24	ad2antrr	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \to (0 ..^N) \subseteq (0 ..^N + 1)$
26	25	sselda	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to i \in (0 ..^N + 1)$
27		oveq2	$⊢ \|T\| = N + 1 \to (0 ..^\|T\|) = (0 ..^N + 1)$
28	27	eleq2d	$⊢ \|T\| = N + 1 \to (i \in (0 ..^\|T\|) \leftrightarrow i \in (0 ..^N + 1))$
29	28	adantl	$⊢ (T \in Word V \land \|T\| = N + 1) \to (i \in (0 ..^\|T\|) \leftrightarrow i \in (0 ..^N + 1))$
30	29	ad2antlr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to (i \in (0 ..^\|T\|) \leftrightarrow i \in (0 ..^N + 1))$
31	26 30	mpbird	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to i \in (0 ..^\|T\|)$
32		ccats1val1	$⊢ (T \in Word V \land i \in (0 ..^\|T\|)) \to (T ++ ⟨“ S ”⟩) (i) = T (i)$
33	23 31 32	syl2anc	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to (T ++ ⟨“ S ”⟩) (i) = T (i)$
34		fzonn0p1p1	$⊢ i \in (0 ..^N) \to i + 1 \in (0 ..^N + 1)$
35	34	adantl	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to i + 1 \in (0 ..^N + 1)$
36	27	adantl	$⊢ (T \in Word V \land \|T\| = N + 1) \to (0 ..^\|T\|) = (0 ..^N + 1)$
37	36	ad2antlr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to (0 ..^\|T\|) = (0 ..^N + 1)$
38	35 37	eleqtrrd	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to i + 1 \in (0 ..^\|T\|)$
39		ccats1val1	$⊢ (T \in Word V \land i + 1 \in (0 ..^\|T\|)) \to (T ++ ⟨“ S ”⟩) (i + 1) = T (i + 1)$
40	23 38 39	syl2anc	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to (T ++ ⟨“ S ”⟩) (i + 1) = T (i + 1)$
41	33 40	preq12d	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land \|T\| = N + 1)) \land i \in (0 ..^N)) \to \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} = \{T (i), T (i + 1)\}$
42	41	exp31	$⊢ (N \in ℕ_{0} \land S \in V) \to ((T \in Word V \land \|T\| = N + 1) \to (i \in (0 ..^N) \to \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} = \{T (i), T (i + 1)\}))$
43	42	adantrr	$⊢ (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to ((T \in Word V \land \|T\| = N + 1) \to (i \in (0 ..^N) \to \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} = \{T (i), T (i + 1)\}))$
44	43	impcom	$⊢ ((T \in Word V \land \|T\| = N + 1) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (i \in (0 ..^N) \to \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} = \{T (i), T (i + 1)\})$
45	44	imp	$⊢ (((T \in Word V \land \|T\| = N + 1) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \land i \in (0 ..^N)) \to \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} = \{T (i), T (i + 1)\}$
46	45	eleq1d	$⊢ (((T \in Word V \land \|T\| = N + 1) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \land i \in (0 ..^N)) \to (\{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow \{T (i), T (i + 1)\} \in E)$
47	46	ralbidva	$⊢ ((T \in Word V \land \|T\| = N + 1) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (\forall i \in (0 ..^N) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E)$
48	47	exbiri	$⊢ (T \in Word V \land \|T\| = N + 1) \to ((N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to (\forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E \to \forall i \in (0 ..^N) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E))$
49	48	com23	$⊢ (T \in Word V \land \|T\| = N + 1) \to (\forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E \to ((N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to \forall i \in (0 ..^N) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E))$
50	49	3impia	$⊢ (T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \to ((N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to \forall i \in (0 ..^N) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E)$
51	50	imp	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \forall i \in (0 ..^N) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E$
52		oveq1	$⊢ \|T\| = N + 1 \to \|T\| - 1 = N + 1 - 1$
53	52	adantl	$⊢ (T \in Word V \land \|T\| = N + 1) \to \|T\| - 1 = N + 1 - 1$
54		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
55		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
56	54 55	pncand	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
57	56	adantl	$⊢ (S \in V \land N \in ℕ_{0}) \to N + 1 - 1 = N$
58	53 57	sylan9eqr	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to \|T\| - 1 = N$
59	58	fveq2d	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to T (\|T\| - 1) = T (N)$
60		lsw	$⊢ T \in Word V \to lastS (T) = T (\|T\| - 1)$
61	60	ad2antrl	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to lastS (T) = T (\|T\| - 1)$
62		simprl	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to T \in Word V$
63		fzonn0p1	$⊢ N \in ℕ_{0} \to N \in (0 ..^N + 1)$
64	63	ad2antlr	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to N \in (0 ..^N + 1)$
65	27	eleq2d	$⊢ \|T\| = N + 1 \to (N \in (0 ..^\|T\|) \leftrightarrow N \in (0 ..^N + 1))$
66	65	ad2antll	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to (N \in (0 ..^\|T\|) \leftrightarrow N \in (0 ..^N + 1))$
67	64 66	mpbird	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to N \in (0 ..^\|T\|)$
68		ccats1val1	$⊢ (T \in Word V \land N \in (0 ..^\|T\|)) \to (T ++ ⟨“ S ”⟩) (N) = T (N)$
69	62 67 68	syl2anc	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to (T ++ ⟨“ S ”⟩) (N) = T (N)$
70	59 61 69	3eqtr4d	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to lastS (T) = (T ++ ⟨“ S ”⟩) (N)$
71		simpll	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to S \in V$
72		simprr	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to \|T\| = N + 1$
73	72	eqcomd	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to N + 1 = \|T\|$
74		ccats1val2	$⊢ (T \in Word V \land S \in V \land N + 1 = \|T\|) \to (T ++ ⟨“ S ”⟩) (N + 1) = S$
75	74	eqcomd	$⊢ (T \in Word V \land S \in V \land N + 1 = \|T\|) \to S = (T ++ ⟨“ S ”⟩) (N + 1)$
76	62 71 73 75	syl3anc	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to S = (T ++ ⟨“ S ”⟩) (N + 1)$
77	70 76	preq12d	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to \{lastS (T), S\} = \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\}$
78	77	eleq1d	$⊢ ((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to (\{lastS (T), S\} \in E \leftrightarrow \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E)$
79	78	biimpcd	$⊢ \{lastS (T), S\} \in E \to (((S \in V \land N \in ℕ_{0}) \land (T \in Word V \land \|T\| = N + 1)) \to \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E)$
80	79	exp4c	$⊢ \{lastS (T), S\} \in E \to (S \in V \to (N \in ℕ_{0} \to ((T \in Word V \land \|T\| = N + 1) \to \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E)))$
81	80	impcom	$⊢ (S \in V \land \{lastS (T), S\} \in E) \to (N \in ℕ_{0} \to ((T \in Word V \land \|T\| = N + 1) \to \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E))$
82	81	impcom	$⊢ (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to ((T \in Word V \land \|T\| = N + 1) \to \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E)$
83	82	impcom	$⊢ ((T \in Word V \land \|T\| = N + 1) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E$
84	83	3adantl3	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E$
85		fveq2	$⊢ i = N \to (T ++ ⟨“ S ”⟩) (i) = (T ++ ⟨“ S ”⟩) (N)$
86		fvoveq1	$⊢ i = N \to (T ++ ⟨“ S ”⟩) (i + 1) = (T ++ ⟨“ S ”⟩) (N + 1)$
87	85 86	preq12d	$⊢ i = N \to \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} = \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\}$
88	87	eleq1d	$⊢ i = N \to (\{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E)$
89	88	ralsng	$⊢ N \in ℕ_{0} \to (\forall i \in \{N\} \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E)$
90	89	ad2antrl	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (\forall i \in \{N\} \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow \{(T ++ ⟨“ S ”⟩) (N), (T ++ ⟨“ S ”⟩) (N + 1)\} \in E)$
91	84 90	mpbird	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \forall i \in \{N\} \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E$
92		ralunb	$⊢ \forall i \in ((0 ..^N) \cup \{N\}) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow (\forall i \in (0 ..^N) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \land \forall i \in \{N\} \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E)$
93	51 91 92	sylanbrc	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \forall i \in ((0 ..^N) \cup \{N\}) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E$
94		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
95		eluzfz2	$⊢ N \in ℤ_{\geq 0} \to N \in (0 \dots N)$
96	94 95	sylbi	$⊢ N \in ℕ_{0} \to N \in (0 \dots N)$
97		fzelp1	$⊢ N \in (0 \dots N) \to N \in (0 \dots N + 1)$
98		fzosplit	$⊢ N \in (0 \dots N + 1) \to (0 ..^N + 1) = (0 ..^N) \cup (N ..^N + 1)$
99	96 97 98	3syl	$⊢ N \in ℕ_{0} \to (0 ..^N + 1) = (0 ..^N) \cup (N ..^N + 1)$
100		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
101		fzosn	$⊢ N \in ℤ \to (N ..^N + 1) = \{N\}$
102	100 101	syl	$⊢ N \in ℕ_{0} \to (N ..^N + 1) = \{N\}$
103	102	uneq2d	$⊢ N \in ℕ_{0} \to (0 ..^N) \cup (N ..^N + 1) = (0 ..^N) \cup \{N\}$
104	99 103	eqtrd	$⊢ N \in ℕ_{0} \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
105	104	ad2antrl	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
106	105	raleqdv	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (\forall i \in (0 ..^N + 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow \forall i \in ((0 ..^N) \cup \{N\}) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E)$
107	93 106	mpbird	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \forall i \in (0 ..^N + 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E$
108		ccatlen	$⊢ (T \in Word V \land ⟨“ S ”⟩ \in Word V) \to \|T ++ ⟨“ S ”⟩\| = \|T\| + \|⟨“ S ”⟩\|$
109	5 20 108	syl2an	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|T ++ ⟨“ S ”⟩\| = \|T\| + \|⟨“ S ”⟩\|$
110	109	oveq1d	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|T ++ ⟨“ S ”⟩\| - 1 = \|T\| + \|⟨“ S ”⟩\| - 1$
111		simpl2	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|T\| = N + 1$
112		s1len	$⊢ \|⟨“ S ”⟩\| = 1$
113	112	a1i	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|⟨“ S ”⟩\| = 1$
114	111 113	oveq12d	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|T\| + \|⟨“ S ”⟩\| = N + 1 + 1$
115	114	oveq1d	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|T\| + \|⟨“ S ”⟩\| - 1 = (N + 1) + 1 - 1$
116		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
117	116	nn0cnd	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
118	117 55	pncand	$⊢ N \in ℕ_{0} \to (N + 1) + 1 - 1 = N + 1$
119	118	ad2antrl	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (N + 1) + 1 - 1 = N + 1$
120	110 115 119	3eqtrd	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|T ++ ⟨“ S ”⟩\| - 1 = N + 1$
121	120	oveq2d	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) = (0 ..^N + 1)$
122	121	raleqdv	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (\forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E \leftrightarrow \forall i \in (0 ..^N + 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E)$
123	107 122	mpbird	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E$
124	18 22 123	3jca	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to (T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E)$
125	109 114	eqtrd	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to \|T ++ ⟨“ S ”⟩\| = N + 1 + 1$
126	124 125	jca	$⊢ ((T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \land (N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E))) \to ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1)$
127	126	ex	$⊢ (T \in Word V \land \|T\| = N + 1 \land \forall i \in (0 ..^N) \{T (i), T (i + 1)\} \in E) \to ((N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
128	4 127	syl	$⊢ T \in (N WWalksN G) \to ((N \in ℕ_{0} \land (S \in V \land \{lastS (T), S\} \in E)) \to ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
129	128	expd	$⊢ T \in (N WWalksN G) \to (N \in ℕ_{0} \to ((S \in V \land \{lastS (T), S\} \in E) \to ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1)))$
130	129	impcom	$⊢ (N \in ℕ_{0} \land T \in (N WWalksN G)) \to ((S \in V \land \{lastS (T), S\} \in E) \to ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
131	130	adantll	$⊢ ((G \in V \land N \in ℕ_{0}) \land T \in (N WWalksN G)) \to ((S \in V \land \{lastS (T), S\} \in E) \to ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
132		iswwlksn	$⊢ N + 1 \in ℕ_{0} \to (T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G) \leftrightarrow (T ++ ⟨“ S ”⟩ \in WWalks (G) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
133	116 132	syl	$⊢ N \in ℕ_{0} \to (T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G) \leftrightarrow (T ++ ⟨“ S ”⟩ \in WWalks (G) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
134	133	adantl	$⊢ (G \in V \land N \in ℕ_{0}) \to (T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G) \leftrightarrow (T ++ ⟨“ S ”⟩ \in WWalks (G) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
135	1 2	iswwlks	$⊢ T ++ ⟨“ S ”⟩ \in WWalks (G) \leftrightarrow (T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E)$
136	135	anbi1i	$⊢ (T ++ ⟨“ S ”⟩ \in WWalks (G) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1) \leftrightarrow ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1)$
137	134 136	bitrdi	$⊢ (G \in V \land N \in ℕ_{0}) \to (T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G) \leftrightarrow ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
138	137	adantr	$⊢ ((G \in V \land N \in ℕ_{0}) \land T \in (N WWalksN G)) \to (T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G) \leftrightarrow ((T ++ ⟨“ S ”⟩ \neq \emptyset \land T ++ ⟨“ S ”⟩ \in Word V \land \forall i \in (0 ..^\|T ++ ⟨“ S ”⟩\| - 1) \{(T ++ ⟨“ S ”⟩) (i), (T ++ ⟨“ S ”⟩) (i + 1)\} \in E) \land \|T ++ ⟨“ S ”⟩\| = N + 1 + 1))$
139	131 138	sylibrd	$⊢ ((G \in V \land N \in ℕ_{0}) \land T \in (N WWalksN G)) \to ((S \in V \land \{lastS (T), S\} \in E) \to T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G))$
140	139	ex	$⊢ (G \in V \land N \in ℕ_{0}) \to (T \in (N WWalksN G) \to ((S \in V \land \{lastS (T), S\} \in E) \to T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G)))$
141	140	3adant3	$⊢ (G \in V \land N \in ℕ_{0} \land T \in Word V) \to (T \in (N WWalksN G) \to ((S \in V \land \{lastS (T), S\} \in E) \to T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G)))$
142	3 141	mpcom	$⊢ T \in (N WWalksN G) \to ((S \in V \land \{lastS (T), S\} \in E) \to T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G))$
143	142	3impib	$⊢ (T \in (N WWalksN G) \land S \in V \land \{lastS (T), S\} \in E) \to T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G)$

Metamath Proof Explorer

Theorem wwlksnext

Proof