clwwlknonex2lem2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > clwwlknonex2lem2		GIF version

Theorem clwwlknonex2lem2 16679

Description: Lemma 2 for clwwlknonex2 16680: 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
clwwlknonex2.v	⊢ 𝑉 = (Vtx‘𝐺)
clwwlknonex2.e	⊢ 𝐸 = (Edg‘𝐺)

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

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

**Proof of Theorem clwwlknonex2lem2**
Step	Hyp	Ref	Expression
1		simpl 109	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑊 ∈ Word 𝑉)
2	1	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝑉)
3		elfzonn0 10598	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 ∈ ℕ₀)
4	3	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈ ℕ₀)
5		lencl 11308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
6		elfzo0 10593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^((♯‘𝑊) − 1)) ↔ (𝑖 ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)))
7		nn0re 9572	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℝ)
8	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → 𝑖 ∈ ℝ)
9		nn0re 9572	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑊) ∈ ℕ₀ → (♯‘𝑊) ∈ ℝ)
10		peano2rem 8593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑊) ∈ ℝ → ((♯‘𝑊) − 1) ∈ ℝ)
11	9, 10	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑊) ∈ ℕ₀ → ((♯‘𝑊) − 1) ∈ ℝ)
12	11	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → ((♯‘𝑊) − 1) ∈ ℝ)
13	9	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → (♯‘𝑊) ∈ ℝ)
14	8, 12, 13	3jca 1208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → (𝑖 ∈ ℝ ∧ ((♯‘𝑊) − 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ))
15	9	ltm1d 9262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑊) ∈ ℕ₀ → ((♯‘𝑊) − 1) < (♯‘𝑊))
16	15	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → ((♯‘𝑊) − 1) < (♯‘𝑊))
17		lttr 8399	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ℝ ∧ ((♯‘𝑊) − 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → ((𝑖 < ((♯‘𝑊) − 1) ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)) → 𝑖 < (♯‘𝑊)))
18	17	expcomd 1491	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ ℝ ∧ ((♯‘𝑊) − 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → (((♯‘𝑊) − 1) < (♯‘𝑊) → (𝑖 < ((♯‘𝑊) − 1) → 𝑖 < (♯‘𝑊))))
19	14, 16, 18	sylc 62	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → (𝑖 < ((♯‘𝑊) − 1) → 𝑖 < (♯‘𝑊)))
20	19	impancom 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ₀ → 𝑖 < (♯‘𝑊)))
21	20	3adant2 1047	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ₀ → 𝑖 < (♯‘𝑊)))
22	6, 21	sylbi 121	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ₀ → 𝑖 < (♯‘𝑊)))
23	5, 22	syl5com 29	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ Word 𝑉 → (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 < (♯‘𝑊)))
24	23	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → 𝑖 < (♯‘𝑊)))
25	24	imp 124	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 < (♯‘𝑊))
26		simplrl 541	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑋 ∈ 𝑉)
27		simplrr 542	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑌 ∈ 𝑉)
28	2, 4, 25, 26, 27	ccat2s1fvwd 11415	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (𝑊‘𝑖))
29	28	eqcomd 2244	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖))
30		peano2nn0 9603	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
31	4, 30	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈ ℕ₀)
32		1red 8341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → 1 ∈ ℝ)
33	8, 32, 13	ltaddsubd 8873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → ((𝑖 + 1) < (♯‘𝑊) ↔ 𝑖 < ((♯‘𝑊) − 1)))
34	33	biimprd 158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀) → (𝑖 < ((♯‘𝑊) − 1) → (𝑖 + 1) < (♯‘𝑊)))
35	34	impancom 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ₀ → (𝑖 + 1) < (♯‘𝑊)))
36	35	3adant2 1047	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧ 𝑖 < ((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ₀ → (𝑖 + 1) < (♯‘𝑊)))
37	6, 36	sylbi 121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (0..^((♯‘𝑊) − 1)) → ((♯‘𝑊) ∈ ℕ₀ → (𝑖 + 1) < (♯‘𝑊)))
38	5, 37	mpan9 281	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) < (♯‘𝑊))
39	38	adantlr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) < (♯‘𝑊))
40	2, 31, 39, 26, 27	ccat2s1fvwd 11415	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
41	40	eqcomd 2244	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑊‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)))
42	29, 41	preq12d 3796	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))})
43	42	eleq1d 2307	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
44	43	ralbidva 2546	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
45	44	biimpd 144	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
46	45	impancom 260	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
47	46	3adant3 1048	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
48	47	3ad2ant1 1049	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
49	48	com12 30	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
50	49	a1dd 48	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
51	50	3adant3 1048	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
52	51	imp31 256	. 2 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
53		ax-1 6	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)))
54	53	3adant3 1048	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)))
55		simpl1l 1079	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → 𝑊 ∈ Word 𝑉)
56		oveq1 6092	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑊) = (𝑁 − 2) → ((♯‘𝑊) − 1) = ((𝑁 − 2) − 1))
57	56	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((♯‘𝑊) − 1) = ((𝑁 − 2) − 1))
58		eluzelcn 9933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℂ)
59		2cnd 9377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 2 ∈ ℂ)
60		1cnd 8342	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ ℂ)
61	58, 59, 60	subsub4d 8668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
62		2p1e3 9438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 + 1) = 3
63	62	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (2 + 1) = 3)
64	63	oveq2d 6101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3))
65		uznn0sub 9954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 3) ∈ ℕ₀)
66	64, 65	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − (2 + 1)) ∈ ℕ₀)
67	61, 66	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑁 − 2) − 1) ∈ ℕ₀)
68	67	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑁 − 2) − 1) ∈ ℕ₀)
69	57, 68	eqeltrd 2315	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑊) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((♯‘𝑊) − 1) ∈ ℕ₀)
70	69	ancoms 268	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → ((♯‘𝑊) − 1) ∈ ℕ₀)
71	70	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → ((♯‘𝑊) − 1) ∈ ℕ₀)
72		simpl 109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → 𝑊 ∈ Word 𝑉)
73	70	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → ((♯‘𝑊) − 1) ∈ ℕ₀)
74	5, 9	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℝ)
75	74	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (♯‘𝑊) ∈ ℝ)
76	75	ltm1d 9262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → ((♯‘𝑊) − 1) < (♯‘𝑊))
77	72, 73, 76	3jca 1208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)))
78	77	ex 115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))))
79	78	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))))
80	79	3ad2ant1 1049	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → ((𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) < (♯‘𝑊))))
81	80	imp 124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ₀ ∧ ((♯‘𝑊) − 1) < (♯‘𝑊)))
82	81	simp3d 1042	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → ((♯‘𝑊) − 1) < (♯‘𝑊))
83		simpl2l 1081	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → 𝑋 ∈ 𝑉)
84		simpl2r 1082	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → 𝑌 ∈ 𝑉)
85	55, 71, 82, 83, 84	ccat2s1fvwd 11415	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
86		nn0cn 9573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑊) ∈ ℕ₀ → (♯‘𝑊) ∈ ℂ)
87		ax-1cn 8272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
88		npcan 8535	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑊) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
89	86, 87, 88	sylancl 417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑊) ∈ ℕ₀ → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
90	5, 89	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ Word 𝑉 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
91	90	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
92	91	3ad2ant1 1049	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
93	92	fveq2d 5699	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)))
94		eqid 2238	. . . . . . . . . . . . . . . . . . . 20 ⊢ (♯‘𝑊) = (♯‘𝑊)
95		ccatw2s1p1g 11413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)) = 𝑋)
96	94, 95	mpanl2 439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)) = 𝑋)
97	96	adantlr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)) = 𝑋)
98	97	3adant3 1048	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)) = 𝑋)
99	93, 98	eqtrd 2271	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)) = 𝑋)
100	99	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)) = 𝑋)
101	85, 100	preq12d 3796	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} = {(𝑊‘((♯‘𝑊) − 1)), 𝑋})
102		lswwrd 11351	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
103	102	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
104		simpl 109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘0) = 𝑋)
105	103, 104	preq12d 3796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → {(lastS‘𝑊), (𝑊‘0)} = {(𝑊‘((♯‘𝑊) − 1)), 𝑋})
106	105	eleq1d 2307	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 ↔ {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸))
107	106	biimpd 144	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘0) = 𝑋 ∧ 𝑊 ∈ Word 𝑉) → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸))
108	107	expcom 116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑊‘0) = 𝑋 → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)))
109	108	com23 78	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ Word 𝑉 → ({(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸 → ((𝑊‘0) = 𝑋 → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)))
110	109	imp31 256	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)
111	110	3adant2 1047	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)
112	111	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → {(𝑊‘((♯‘𝑊) − 1)), 𝑋} ∈ 𝐸)
113	101, 112	eqeltrd 2315	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑊‘0) = 𝑋) ∧ (𝑁 ∈ (ℤ_≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2))) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)
114	113	exp520 1259	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → (𝑁 ∈ (ℤ_≥‘3) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
115	114	com14 88	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
116	115	3ad2ant3 1051	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
117	54, 116	syld 45	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
118	117	com25 91	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
119	118	com14 88	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
120	119	3adant2 1047	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((♯‘𝑊) = (𝑁 − 2) → ((𝑊‘0) = 𝑋 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))))
121	120	3imp 1224	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)))
122	121	impcom 125	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))
123	122	imp 124	. . 3 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸)
124		ccatw2s1p2 11414	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1)) = 𝑌)
125	94, 124	mpanl2 439	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1)) = 𝑌)
126	96, 125	preq12d 3796	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})
127	126	expcom 116	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌}))
128	127	a1i 9	. . . . . . . . . 10 ⊢ ({𝑋, 𝑌} ∈ 𝐸 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
129	128	com13 80	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
130	129	3ad2ant1 1049	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
131	130	3ad2ant1 1049	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
132	131	com12 30	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
133	132	3adant3 1048	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑋, 𝑌} ∈ 𝐸 → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})))
134	133	imp31 256	. . . 4 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} = {𝑋, 𝑌})
135		simpr 110	. . . 4 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {𝑋, 𝑌} ∈ 𝐸)
136	134, 135	eqeltrd 2315	. . 3 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)
137	5	nn0zd 9766	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ)
138		1zzd 9671	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → 1 ∈ ℤ)
139	137, 138	zsubcld 9773	. . . . . . . 8 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) − 1) ∈ ℤ)
140		fveq2 5695	. . . . . . . . . . 11 ⊢ (𝑖 = ((♯‘𝑊) − 1) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)))
141		fvoveq1 6108	. . . . . . . . . . 11 ⊢ (𝑖 = ((♯‘𝑊) − 1) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1)))
142	140, 141	preq12d 3796	. . . . . . . . . 10 ⊢ (𝑖 = ((♯‘𝑊) − 1) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))})
143	142	eleq1d 2307	. . . . . . . . 9 ⊢ (𝑖 = ((♯‘𝑊) − 1) → ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸))
144		fveq2 5695	. . . . . . . . . . 11 ⊢ (𝑖 = (♯‘𝑊) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)))
145		fvoveq1 6108	. . . . . . . . . . 11 ⊢ (𝑖 = (♯‘𝑊) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1)))
146	144, 145	preq12d 3796	. . . . . . . . . 10 ⊢ (𝑖 = (♯‘𝑊) → {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} = {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))})
147	146	eleq1d 2307	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝑊) → ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸))
148	143, 147	ralprg 3760	. . . . . . . 8 ⊢ ((((♯‘𝑊) − 1) ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ₀) → (∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)))
149	139, 5, 148	syl2anc 415	. . . . . . 7 ⊢ (𝑊 ∈ Word 𝑉 → (∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)))
150	149	3ad2ant1 1049	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) → (∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)))
151	150	3ad2ant1 1049	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)))
152	151	adantl 277	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → (∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)))
153	152	adantr 276	. . 3 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → (∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) − 1)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(♯‘𝑊)), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((♯‘𝑊) + 1))} ∈ 𝐸)))
154	123, 136, 153	mpbir2and 957	. 2 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
155		ralunb 3410	. 2 ⊢ (∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1), (♯‘𝑊)} {(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸))
156	52, 154, 155	sylanbrc 421	1 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 ∀wral 2528 ∪ cun 3218 {cpr 3710 class class class wbr 4130 ‘cfv 5377 (class class class)co 6085 ℂcc 8177 ℝcr 8178 0cc0 8179 1c1 8180 + caddc 8182 < clt 8360 − cmin 8497 ℕcn 9304 2c2 9355 3c3 9356 ℕ₀cn0 9563 ℤcz 9644 ℤ_≥cuz 9921 ..^cfzo 10549 ♯chash 11214 Word cword 11304 lastSclsw 11349 ++ cconcat 11358 ⟨“cs1 11383 Vtxcvtx 16253 Edgcedg 16298

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-addcom 8279 ax-addass 8281 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-0id 8287 ax-rnegex 8288 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-1o 6687 df-er 6807 df-en 7023 df-dom 7024 df-fin 7025 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-inn 9305 df-2 9363 df-3 9364 df-n0 9564 df-z 9645 df-uz 9922 df-fz 10412 df-fzo 10550 df-ihash 11215 df-word 11305 df-lsw 11350 df-concat 11359 df-s1 11384

This theorem is used by: clwwlknonex2 16680

W3C validator