clwwlkext2edg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > clwwlkext2edg		Structured version Visualization version GIF version

Theorem clwwlkext2edg 29309

Description: If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)

**Hypotheses**
Ref	Expression
clwwlkext2edg.v	⊢ 𝑉 = (Vtx‘𝐺)
clwwlkext2edg.e	⊢ 𝐸 = (Edg‘𝐺)

**Assertion**
Ref	Expression
clwwlkext2edg	⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (𝑊 ++ ⟨“𝑍”⟩) ∈ (𝑁 ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸))

Proof of Theorem clwwlkext2edg Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		clwwlknnn 29286	. . 3 ⊢ ((𝑊 ++ ⟨“𝑍”⟩) ∈ (𝑁 ClWWalksN 𝐺) → 𝑁 ∈ ℕ)
2		clwwlkext2edg.v	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
3		clwwlkext2edg.e	. . . . 5 ⊢ 𝐸 = (Edg‘𝐺)
4	2, 3	isclwwlknx 29289	. . . 4 ⊢ (𝑁 ∈ ℕ → ((𝑊 ++ ⟨“𝑍”⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁)))
5		ige2m2fzo 13695	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (𝑁 − 2) ∈ (0..^(𝑁 − 1)))
6	5	3ad2ant3 1136	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑁 − 2) ∈ (0..^(𝑁 − 1)))
7	6	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (𝑁 − 2) ∈ (0..^(𝑁 − 1)))
8		oveq1 7416	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (𝑁 − 1))
9	8	oveq2d 7425	. . . . . . . . . . . . . . 15 ⊢ ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) = (0..^(𝑁 − 1)))
10	9	eleq2d 2820	. . . . . . . . . . . . . 14 ⊢ ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → ((𝑁 − 2) ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) ↔ (𝑁 − 2) ∈ (0..^(𝑁 − 1))))
11	10	adantl 483	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑁 − 2) ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) ↔ (𝑁 − 2) ∈ (0..^(𝑁 − 1))))
12	7, 11	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (𝑁 − 2) ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)))
13		fveq2 6892	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑁 − 2) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)))
14		fvoveq1 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑁 − 2) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1)))
15	13, 14	preq12d 4746	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑁 − 2) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)), ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1))})
16	15	eleq1d 2819	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑁 − 2) → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)), ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1))} ∈ 𝐸))
17	16	rspcv 3609	. . . . . . . . . . . 12 ⊢ ((𝑁 − 2) ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 → {((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)), ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1))} ∈ 𝐸))
18	12, 17	syl 17	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 → {((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)), ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1))} ∈ 𝐸))
19		wrdlenccats1lenm1 14572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (♯‘𝑊))
20	19	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) = ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1))
21	20	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (♯‘𝑊) = ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1))
22	21, 8	sylan9eq 2793	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (♯‘𝑊) = (𝑁 − 1))
23	22	ex 414	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → (♯‘𝑊) = (𝑁 − 1)))
24	23	3adant3 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → (♯‘𝑊) = (𝑁 − 1)))
25		eluzelcn 12834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 𝑁 ∈ ℂ)
26		1cnd 11209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 ∈ ℂ)
27	25, 26, 26	subsub4d 11602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1)))
28		1p1e2 12337	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 + 1) = 2
29	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (1 + 1) = 2)
30	29	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (𝑁 − (1 + 1)) = (𝑁 − 2))
31	27, 30	eqtr2d 2774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (𝑁 − 2) = ((𝑁 − 1) − 1))
32	31	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑁 − 2) = ((𝑁 − 1) − 1))
33		oveq1 7416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑊) = (𝑁 − 1) → ((♯‘𝑊) − 1) = ((𝑁 − 1) − 1))
34	33	eqcomd 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑊) = (𝑁 − 1) → ((𝑁 − 1) − 1) = ((♯‘𝑊) − 1))
35	32, 34	sylan9eq 2793	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → (𝑁 − 2) = ((♯‘𝑊) − 1))
36	35	ex 414	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘𝑊) = (𝑁 − 1) → (𝑁 − 2) = ((♯‘𝑊) − 1)))
37	24, 36	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → (𝑁 − 2) = ((♯‘𝑊) − 1)))
38	37	imp 408	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (𝑁 − 2) = ((♯‘𝑊) − 1))
39	38	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)) = ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)))
40		simpl1 1192	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → 𝑊 ∈ Word 𝑉)
41		s1cl 14552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑍 ∈ 𝑉 → ⟨“𝑍”⟩ ∈ Word 𝑉)
42	41	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
43	42	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
44		eluz2 12828	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁))
45		zre 12562	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
46		1red 11215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 1 ∈ ℝ)
47		2re 12286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 2 ∈ ℝ
48	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 2 ∈ ℝ)
49		simpl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 𝑁 ∈ ℝ)
50		1lt2 12383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 < 2
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 1 < 2)
52		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 2 ≤ 𝑁)
53	46, 48, 49, 51, 52	ltletrd 11374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 1 < 𝑁)
54		1red 11215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑁 ∈ ℝ → 1 ∈ ℝ)
55		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑁 ∈ ℝ → 𝑁 ∈ ℝ)
56	54, 55	posdifd 11801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℝ → (1 < 𝑁 ↔ 0 < (𝑁 − 1)))
57	56	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → (1 < 𝑁 ↔ 0 < (𝑁 − 1)))
58	53, 57	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 0 < (𝑁 − 1))
59	58	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℝ → (2 ≤ 𝑁 → 0 < (𝑁 − 1)))
60	45, 59	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℤ → (2 ≤ 𝑁 → 0 < (𝑁 − 1)))
61	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 ∈ ℤ → (𝑁 ∈ ℤ → (2 ≤ 𝑁 → 0 < (𝑁 − 1))))
62	61	3imp 1112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁) → 0 < (𝑁 − 1))
63	44, 62	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 0 < (𝑁 − 1))
64	63	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → 0 < (𝑁 − 1))
65		breq2 5153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑊) = (𝑁 − 1) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 − 1)))
66	65	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 − 1)))
67	64, 66	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → 0 < (♯‘𝑊))
68		hashneq0 14324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ Word 𝑉 → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
69	68	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
70	69	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
71	67, 70	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → 𝑊 ≠ ∅)
72	71	3adantl2 1168	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → 𝑊 ≠ ∅)
73	40, 43, 72	3jca 1129	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → (𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅))
74	73	ex 414	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘𝑊) = (𝑁 − 1) → (𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)))
75	24, 74	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → (𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)))
76	75	imp 408	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅))
77		ccatval1lsw 14534	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
78	76, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
79	39, 78	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)) = (lastS‘𝑊))
80		2m1e1 12338	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 − 1) = 1
81	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (2 − 1) = 1)
82	81	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 = (2 − 1))
83	82	oveq2d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (𝑁 − 1) = (𝑁 − (2 − 1)))
84		2cnd 12290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 2 ∈ ℂ)
85	25, 84, 26	subsubd 11599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (𝑁 − (2 − 1)) = ((𝑁 − 2) + 1))
86	83, 85	eqtr2d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − 1))
87	86	3ad2ant3 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((𝑁 − 2) + 1) = (𝑁 − 1))
88		eqeq2 2745	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑊) = (𝑁 − 1) → (((𝑁 − 2) + 1) = (♯‘𝑊) ↔ ((𝑁 − 2) + 1) = (𝑁 − 1)))
89	87, 88	syl5ibrcom 246	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘𝑊) = (𝑁 − 1) → ((𝑁 − 2) + 1) = (♯‘𝑊)))
90	24, 89	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → ((𝑁 − 2) + 1) = (♯‘𝑊)))
91	90	imp 408	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑁 − 2) + 1) = (♯‘𝑊))
92	91	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)))
93		id 22	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
94	93	3adant3 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
95	94	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
96		ccatws1ls 14583	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
97	95, 96	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
98	92, 97	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1)) = 𝑍)
99	79, 98	preq12d 4746	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)), ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1))} = {(lastS‘𝑊), 𝑍})
100	99	eleq1d 2819	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ({((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 − 2)), ((𝑊 ++ ⟨“𝑍”⟩)‘((𝑁 − 2) + 1))} ∈ 𝐸 ↔ {(lastS‘𝑊), 𝑍} ∈ 𝐸))
101	18, 100	sylibd 238	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 → {(lastS‘𝑊), 𝑍} ∈ 𝐸))
102	101	ex 414	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 → {(lastS‘𝑊), 𝑍} ∈ 𝐸)))
103	102	com13 88	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → {(lastS‘𝑊), 𝑍} ∈ 𝐸)))
104	103	3ad2ant2 1135	. . . . . . 7 ⊢ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → {(lastS‘𝑊), 𝑍} ∈ 𝐸)))
105	104	imp31 419	. . . . . 6 ⊢ (((((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2))) → {(lastS‘𝑊), 𝑍} ∈ 𝐸)
106	94	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
107		lswccats1 14584	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
108	106, 107	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
109	63	3ad2ant3 1136	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → 0 < (𝑁 − 1))
110	109	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → 0 < (𝑁 − 1))
111	65	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 − 1)))
112	110, 111	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → 0 < (♯‘𝑊))
113		ccatfv0 14533	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
114	40, 43, 112, 113	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
115	108, 114	preq12d 4746	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (♯‘𝑊) = (𝑁 − 1)) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)})
116	115	ex 414	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘𝑊) = (𝑁 − 1) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)}))
117	24, 116	syld 47	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)}))
118	117	impcom 409	. . . . . . . . . 10 ⊢ (((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2))) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)})
119	118	eleq1d 2819	. . . . . . . . 9 ⊢ (((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2))) → ({(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸 ↔ {𝑍, (𝑊‘0)} ∈ 𝐸))
120	119	biimpcd 248	. . . . . . . 8 ⊢ ({(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸 → (((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2))) → {𝑍, (𝑊‘0)} ∈ 𝐸))
121	120	3ad2ant3 1136	. . . . . . 7 ⊢ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) → (((♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2))) → {𝑍, (𝑊‘0)} ∈ 𝐸))
122	121	impl 457	. . . . . 6 ⊢ (((((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2))) → {𝑍, (𝑊‘0)} ∈ 𝐸)
123	105, 122	jca 513	. . . . 5 ⊢ (((((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2))) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸))
124	123	ex 414	. . . 4 ⊢ ((((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑁) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)))
125	4, 124	syl6bi 253	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑊 ++ ⟨“𝑍”⟩) ∈ (𝑁 ClWWalksN 𝐺) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸))))
126	1, 125	mpcom 38	. 2 ⊢ ((𝑊 ++ ⟨“𝑍”⟩) ∈ (𝑁 ClWWalksN 𝐺) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)))
127	126	impcom 409	1 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) ∧ (𝑊 ++ ⟨“𝑍”⟩) ∈ (𝑁 ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∅c0 4323 {cpr 4631 class class class wbr 5149 ‘cfv 6544 (class class class)co 7409 ℝcr 11109 0cc0 11110 1c1 11111 + caddc 11113 < clt 11248 ≤ cle 11249 − cmin 11444 ℕcn 12212 2c2 12267 ℤcz 12558 ℤ_≥cuz 12822 ..^cfzo 13627 ♯chash 14290 Word cword 14464 lastSclsw 14512 ++ cconcat 14520 ⟨“cs1 14545 Vtxcvtx 28256 Edgcedg 28307 ClWWalksN cclwwlkn 29277

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-oadd 8470 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-2 12275 df-n0 12473 df-xnn0 12545 df-z 12559 df-uz 12823 df-rp 12975 df-fz 13485 df-fzo 13628 df-hash 14291 df-word 14465 df-lsw 14513 df-concat 14521 df-s1 14546 df-clwwlk 29235 df-clwwlkn 29278

This theorem is referenced by: numclwwlk2lem1 29629

W3C validator