numclwwlkovf2exlem2 - Metamath Proof Explorer

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

Theorem numclwwlkovf2exlem2 27212

Description: Lemma 2 for numclwwlkovf2ex 27219: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.)

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

**Assertion**
Ref	Expression
numclwwlkovf2exlem2	⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ ((0..^((#‘𝑊) − 1)) ∪ {((#‘𝑊) − 1), (#‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)

Distinct variable groups: 𝑖,𝐸 𝑖,𝑉 𝑖,𝑊 𝑖,𝑋 𝑖,𝑌 Allowed substitution hints: 𝐺(𝑖) 𝑁(𝑖)

**Proof of Theorem numclwwlkovf2exlem2**
Step	Hyp	Ref	Expression
1		numclwwlkovf2exlem2.v	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
2	1	nbgrisvtx 26255	. . . . . . . 8 ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑌 ∈ 𝑉)
3		simpll 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → 𝑊 ∈ Word 𝑉)
4		elfzonn0 12512	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^((#‘𝑊) − 1)) → 𝑖 ∈ ℕ₀)
5	4	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → 𝑖 ∈ ℕ₀)
6		lencl 13324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℕ₀)
7		elfzo0 12508	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ (0..^((#‘𝑊) − 1)) ↔ (𝑖 ∈ ℕ₀ ∧ ((#‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑊) − 1)))
8		nn0re 11301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℝ)
9	8	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → 𝑖 ∈ ℝ)
10		nn0re 11301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((#‘𝑊) ∈ ℕ₀ → (#‘𝑊) ∈ ℝ)
11		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((#‘𝑊) ∈ ℝ → ((#‘𝑊) − 1) ∈ ℝ)
12	10, 11	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝑊) ∈ ℕ₀ → ((#‘𝑊) − 1) ∈ ℝ)
13	12	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → ((#‘𝑊) − 1) ∈ ℝ)
14	10	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → (#‘𝑊) ∈ ℝ)
15	9, 13, 14	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → (𝑖 ∈ ℝ ∧ ((#‘𝑊) − 1) ∈ ℝ ∧ (#‘𝑊) ∈ ℝ))
16	10	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((#‘𝑊) ∈ ℕ₀ → ((#‘𝑊) − 1) < (#‘𝑊))
17	16	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → ((#‘𝑊) − 1) < (#‘𝑊))
18		lttr 10114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 ∈ ℝ ∧ ((#‘𝑊) − 1) ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((𝑖 < ((#‘𝑊) − 1) ∧ ((#‘𝑊) − 1) < (#‘𝑊)) → 𝑖 < (#‘𝑊)))
19	18	expcomd 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ ℝ ∧ ((#‘𝑊) − 1) ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → (((#‘𝑊) − 1) < (#‘𝑊) → (𝑖 < ((#‘𝑊) − 1) → 𝑖 < (#‘𝑊))))
20	15, 17, 19	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → (𝑖 < ((#‘𝑊) − 1) → 𝑖 < (#‘𝑊)))
21	20	impancom 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑖 < ((#‘𝑊) − 1)) → ((#‘𝑊) ∈ ℕ₀ → 𝑖 < (#‘𝑊)))
22	21	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ ℕ₀ ∧ ((#‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑊) − 1)) → ((#‘𝑊) ∈ ℕ₀ → 𝑖 < (#‘𝑊)))
23	7, 22	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (0..^((#‘𝑊) − 1)) → ((#‘𝑊) ∈ ℕ₀ → 𝑖 < (#‘𝑊)))
24	6, 23	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑊) − 1)) → 𝑖 < (#‘𝑊)))
25	24	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑖 ∈ (0..^((#‘𝑊) − 1)) → 𝑖 < (#‘𝑊)))
26	25	imp 445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → 𝑖 < (#‘𝑊))
27		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))
28		ccat2s1fvw 13415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ ℕ₀ ∧ 𝑖 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (𝑊‘𝑖))
29	3, 5, 26, 27, 28	syl31anc 1329	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (𝑊‘𝑖))
30	29	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (𝑊‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖))
31		simpl 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → 𝑊 ∈ Word 𝑉)
32		peano2nn0 11333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
33	32	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ ℕ₀ ∧ ((#‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑊) − 1)) → (𝑖 + 1) ∈ ℕ₀)
34	7, 33	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (0..^((#‘𝑊) − 1)) → (𝑖 + 1) ∈ ℕ₀)
35	34	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (𝑖 + 1) ∈ ℕ₀)
36		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → 1 ∈ ℝ)
37	9, 36, 14	ltaddsubd 10627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → ((𝑖 + 1) < (#‘𝑊) ↔ 𝑖 < ((#‘𝑊) − 1)))
38	37	biimprd 238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → (𝑖 < ((#‘𝑊) − 1) → (𝑖 + 1) < (#‘𝑊)))
39	38	impancom 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑖 < ((#‘𝑊) − 1)) → ((#‘𝑊) ∈ ℕ₀ → (𝑖 + 1) < (#‘𝑊)))
40	39	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ ℕ₀ ∧ ((#‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑊) − 1)) → ((#‘𝑊) ∈ ℕ₀ → (𝑖 + 1) < (#‘𝑊)))
41	7, 40	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (0..^((#‘𝑊) − 1)) → ((#‘𝑊) ∈ ℕ₀ → (𝑖 + 1) < (#‘𝑊)))
42	6, 41	mpan9 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (𝑖 + 1) < (#‘𝑊))
43	31, 35, 42	3jca 1242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ₀ ∧ (𝑖 + 1) < (#‘𝑊)))
44	43	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ₀ ∧ (𝑖 + 1) < (#‘𝑊)))
45		ccat2s1fvw 13415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ₀ ∧ (𝑖 + 1) < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
46	44, 27, 45	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
47	46	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → (𝑊‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)))
48	30, 47	preq12d 4276	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))})
49	48	eleq1d 2686	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((#‘𝑊) − 1))) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
50	49	ralbidva 2985	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
51	50	biimpd 219	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
52	51	impancom 456	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
53	52	3adant3 1081	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
54	53	3ad2ant1 1082	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
55	54	com12 32	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
56	55	expcom 451	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑉 → (𝑋 ∈ 𝑉 → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
57	56	com23 86	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑉 → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑋 ∈ 𝑉 → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
58	2, 57	syl 17	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑋 ∈ 𝑉 → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
59	58	ex 450	. . . . . 6 ⊢ (𝐺 ∈ USGraph → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑋 ∈ 𝑉 → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
60	59	com24 95	. . . . 5 ⊢ (𝐺 ∈ USGraph → (𝑋 ∈ 𝑉 → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
61	60	imp 445	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
62	61	3adant3 1081	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
63	62	imp31 448	. 2 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
64	2	ex 450	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → 𝑌 ∈ 𝑉))
65	64	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → 𝑌 ∈ 𝑉))
66		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
67	65, 66	jctild 566	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)))
68	67	3adant3 1081	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)))
69		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → 𝑊 ∈ Word 𝑉)
70		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑊) = (𝑁 − 2) → ((#‘𝑊) − 1) = ((𝑁 − 2) − 1))
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((#‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((#‘𝑊) − 1) = ((𝑁 − 2) − 1))
72		eluzelcn 11699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℂ)
73		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 2 ∈ ℂ)
74		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ ℂ)
75	72, 73, 74	subsub4d 10423	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
76		2p1e3 11151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2 + 1) = 3
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (2 + 1) = 3)
78	77	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3))
79		uznn0sub 11719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 3) ∈ ℕ₀)
80	78, 79	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − (2 + 1)) ∈ ℕ₀)
81	75, 80	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑁 − 2) − 1) ∈ ℕ₀)
82	81	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((#‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑁 − 2) − 1) ∈ ℕ₀)
83	71, 82	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((#‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((#‘𝑊) − 1) ∈ ℕ₀)
84	83	ancoms 469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2)) → ((#‘𝑊) − 1) ∈ ℕ₀)
85	84	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → ((#‘𝑊) − 1) ∈ ℕ₀)
86	6, 10	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℝ)
87	86	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → (#‘𝑊) ∈ ℝ)
88	87	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → ((#‘𝑊) − 1) < (#‘𝑊))
89	69, 85, 88	3jca 1242	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ ℕ₀ ∧ ((#‘𝑊) − 1) < (#‘𝑊)))
90	89	ex 450	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ ℕ₀ ∧ ((#‘𝑊) − 1) < (#‘𝑊))))
91	90	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ ℕ₀ ∧ ((#‘𝑊) − 1) < (#‘𝑊))))
92	91	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → ((𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ ℕ₀ ∧ ((#‘𝑊) − 1) < (#‘𝑊))))
93	92	imp 445	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ ℕ₀ ∧ ((#‘𝑊) − 1) < (#‘𝑊)))
94		simpl2 1065	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))
95		ccat2s1fvw 13415	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ ℕ₀ ∧ ((#‘𝑊) − 1) < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)) = (𝑊‘((#‘𝑊) − 1)))
96	93, 94, 95	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)) = (𝑊‘((#‘𝑊) − 1)))
97		nn0cn 11302	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑊) ∈ ℕ₀ → (#‘𝑊) ∈ ℂ)
98		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
99		npcan 10290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((#‘𝑊) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑊) − 1) + 1) = (#‘𝑊))
100	97, 98, 99	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝑊) ∈ ℕ₀ → (((#‘𝑊) − 1) + 1) = (#‘𝑊))
101	6, 100	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ Word 𝑉 → (((#‘𝑊) − 1) + 1) = (#‘𝑊))
102	101	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → (((#‘𝑊) − 1) + 1) = (#‘𝑊))
103	102	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((#‘𝑊) − 1) + 1) = (#‘𝑊))
104	103	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)))
105		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (#‘𝑊) = (#‘𝑊)
106	105	2a1i 12	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ Word 𝑉 → ({( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸 → (#‘𝑊) = (#‘𝑊)))
107	106	imdistani 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊)))
108	107	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊)))
109		simp2l 1087	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → 𝑋 ∈ 𝑉)
110		simp2r 1088	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → 𝑌 ∈ 𝑉)
111		ccatw2s1p1 13413	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)) = 𝑋)
112	108, 109, 110, 111	syl12anc 1324	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)) = 𝑋)
113	104, 112	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1)) = 𝑋)
114	113	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1)) = 𝑋)
115	96, 114	preq12d 4276	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} = {(𝑊‘((#‘𝑊) − 1)), 𝑋})
116		lsw 13351	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ Word 𝑉 → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1)))
117	116	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1)))
118		simpl 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘0) = 𝑋)
119	117, 118	preq12d 4276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → {( lastS ‘𝑊), (𝑊‘0)} = {(𝑊‘((#‘𝑊) − 1)), 𝑋})
120	119	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → ({( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸 ↔ {(𝑊‘((#‘𝑊) − 1)), 𝑋} ∈ 𝐸))
121	120	biimpd 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → ({( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((#‘𝑊) − 1)), 𝑋} ∈ 𝐸))
122	121	expcom 451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑊‘0) = 𝑋 → ({( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((#‘𝑊) − 1)), 𝑋} ∈ 𝐸)))
123	122	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ Word 𝑉 → ({( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸 → ((𝑊‘0) = 𝑋 → {(𝑊‘((#‘𝑊) − 1)), 𝑋} ∈ 𝐸)))
124	123	imp31 448	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((#‘𝑊) − 1)), 𝑋} ∈ 𝐸)
125	124	3adant2 1080	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((#‘𝑊) − 1)), 𝑋} ∈ 𝐸)
126	125	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → {(𝑊‘((#‘𝑊) − 1)), 𝑋} ∈ 𝐸)
127	115, 126	eqeltrd 2701	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (#‘𝑊) = (𝑁 − 2))) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)
128	127	exp520 1288	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → (𝑁 ∈ (ℤ_≥‘3) → ((#‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))))
129	128	com14 96	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((#‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))))
130	129	3ad2ant3 1084	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((#‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))))
131	68, 130	syld 47	. . . . . . . . 9 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((#‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))))
132	131	com25 99	. . . . . . . 8 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((#‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))))
133	132	com14 96	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((#‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))))
134	133	3adant2 1080	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((#‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))))
135	134	3imp 1256	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)))
136	135	impcom 446	. . . 4 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸))
137	136	imp 445	. . 3 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸)
138	105, 111	mpanl2 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)) = 𝑋)
139		ccatw2s1p2 13414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1)) = 𝑌)
140	105, 139	mpanl2 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1)) = 𝑌)
141	138, 140	preq12d 4276	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})
142	141	expcom 451	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌}))
143	142	expcom 451	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝑉 → (𝑋 ∈ 𝑉 → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})))
144	64, 143	syl6 35	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USGraph → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌}))))
145	144	com24 95	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USGraph → (𝑊 ∈ Word 𝑉 → (𝑋 ∈ 𝑉 → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌}))))
146	145	com12 32	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝑉 → (𝐺 ∈ USGraph → (𝑋 ∈ 𝑉 → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌}))))
147	146	impd 447	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})))
148	147	3ad2ant1 1082	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})))
149	148	3ad2ant1 1082	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})))
150	149	com12 32	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})))
151	150	3adant3 1081	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})))
152	151	imp31 448	. . . 4 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} = {𝑋, 𝑌})
153		numclwwlkovf2exlem2.e	. . . . . . . . 9 ⊢ 𝐸 = (Edg‘𝐺)
154	153	nbusgreledg 26249	. . . . . . . 8 ⊢ (𝐺 ∈ USGraph → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑌, 𝑋} ∈ 𝐸))
155		prcom 4267	. . . . . . . . . 10 ⊢ {𝑌, 𝑋} = {𝑋, 𝑌}
156	155	eleq1i 2692	. . . . . . . . 9 ⊢ ({𝑌, 𝑋} ∈ 𝐸 ↔ {𝑋, 𝑌} ∈ 𝐸)
157	156	biimpi 206	. . . . . . . 8 ⊢ ({𝑌, 𝑋} ∈ 𝐸 → {𝑋, 𝑌} ∈ 𝐸)
158	154, 157	syl6bi 243	. . . . . . 7 ⊢ (𝐺 ∈ USGraph → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑌} ∈ 𝐸))
159	158	3ad2ant1 1082	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑌} ∈ 𝐸))
160	159	adantr 481	. . . . 5 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑌} ∈ 𝐸))
161	160	imp 445	. . . 4 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑋, 𝑌} ∈ 𝐸)
162	152, 161	eqeltrd 2701	. . 3 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} ∈ 𝐸)
163		ovex 6678	. . . 4 ⊢ ((#‘𝑊) − 1) ∈ V
164		fvex 6201	. . . 4 ⊢ (#‘𝑊) ∈ V
165		fveq2 6191	. . . . . 6 ⊢ (𝑖 = ((#‘𝑊) − 1) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)))
166		oveq1 6657	. . . . . . 7 ⊢ (𝑖 = ((#‘𝑊) − 1) → (𝑖 + 1) = (((#‘𝑊) − 1) + 1))
167	166	fveq2d 6195	. . . . . 6 ⊢ (𝑖 = ((#‘𝑊) − 1) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1)))
168	165, 167	preq12d 4276	. . . . 5 ⊢ (𝑖 = ((#‘𝑊) − 1) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))})
169	168	eleq1d 2686	. . . 4 ⊢ (𝑖 = ((#‘𝑊) − 1) → ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸))
170		fveq2 6191	. . . . . 6 ⊢ (𝑖 = (#‘𝑊) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)))
171		oveq1 6657	. . . . . . 7 ⊢ (𝑖 = (#‘𝑊) → (𝑖 + 1) = ((#‘𝑊) + 1))
172	171	fveq2d 6195	. . . . . 6 ⊢ (𝑖 = (#‘𝑊) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1)))
173	170, 172	preq12d 4276	. . . . 5 ⊢ (𝑖 = (#‘𝑊) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))})
174	173	eleq1d 2686	. . . 4 ⊢ (𝑖 = (#‘𝑊) → ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} ∈ 𝐸))
175	163, 164, 169, 174	ralpr 4238	. . 3 ⊢ (∀𝑖 ∈ {((#‘𝑊) − 1), (#‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((#‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(#‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((#‘𝑊) + 1))} ∈ 𝐸))
176	137, 162, 175	sylanbrc 698	. 2 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ {((#‘𝑊) − 1), (#‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
177		ralunb 3794	. 2 ⊢ (∀𝑖 ∈ ((0..^((#‘𝑊) − 1)) ∪ {((#‘𝑊) − 1), (#‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑊) − 1), (#‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
178	63, 176, 177	sylanbrc 698	1 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ ((0..^((#‘𝑊) − 1)) ∪ {((#‘𝑊) − 1), (#‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∪ cun 3572 {cpr 4179 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 < clt 10074 − cmin 10266 ℕcn 11020 2c2 11070 3c3 11071 ℕ₀cn0 11292 ℤ_≥cuz 11687 ..^cfzo 12465 #chash 13117 Word cword 13291 lastS clsw 13292 ++ cconcat 13293 ⟨“cs1 13294 Vtxcvtx 25874 Edgcedg 25939 USGraph cusgr 26044 NeighbVtx cnbgr 26224

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-lsw 13300 df-concat 13301 df-s1 13302 df-edg 25940 df-upgr 25977 df-umgr 25978 df-usgr 26046 df-nbgr 26228

This theorem is referenced by: numclwwlkovf2ex 27219

W3C validator