Theorem clwlkclwwlklem2

Description: Lemma 2 for clwlkclwwlk . (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 11-Apr-2021)

	Ref	Expression
Assertion	clwlkclwwlklem2	⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		f1fn	⊢ ( 𝐸 : dom 𝐸 –1-1→ 𝑅 → 𝐸 Fn dom 𝐸 )
2		dffn3	⊢ ( 𝐸 Fn dom 𝐸 ↔ 𝐸 : dom 𝐸 ⟶ ran 𝐸 )
3	1 2	sylib	⊢ ( 𝐸 : dom 𝐸 –1-1→ 𝑅 → 𝐸 : dom 𝐸 ⟶ ran 𝐸 )
4		lencl	⊢ ( 𝐹 ∈ Word dom 𝐸 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
5		ffn	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
6		fnfz0hash	⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
7	4 5 6	syl2an	⊢ ( ( 𝐹 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
8		ffz0iswrd	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → 𝑃 ∈ Word 𝑉 )
9		lsw	⊢ ( 𝑃 ∈ Word 𝑉 → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
10	9	ad6antr	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
11		fvoveq1	⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) )
12	11	ad4antlr	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) )
13		eqcom	⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) )
14		nn0cn	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
15		1cnd	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 1 ∈ ℂ )
16	14 15	pncand	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) = ( ♯ ‘ 𝐹 ) )
17	16	eqcomd	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) )
18	17	ad4antlr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) )
19	18	fveqeq2d	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) = ( 𝑃 ‘ 0 ) ) )
20	19	biimpd	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) → ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) = ( 𝑃 ‘ 0 ) ) )
21	13 20	biimtrid	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) = ( 𝑃 ‘ 0 ) ) )
22	21	adantld	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) = ( 𝑃 ‘ 0 ) ) )
23	22	imp	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) = ( 𝑃 ‘ 0 ) )
24	10 12 23	3eqtrd	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) )
25		nn0z	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
26		peano2zm	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℤ )
27	25 26	syl	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℤ )
28		nn0re	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℝ )
29	28	lem1d	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) − 1 ) ≤ ( ♯ ‘ 𝐹 ) )
30		eluz2	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ↔ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ≤ ( ♯ ‘ 𝐹 ) ) )
31	27 25 29 30	syl3anbrc	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
32	31	ad4antlr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
33		fzoss2	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
34		ssralv	⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
35	32 33 34	3syl	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
36		simpr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → 𝐸 : dom 𝐸 ⟶ ran 𝐸 )
37	36	adantr	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → 𝐸 : dom 𝐸 ⟶ ran 𝐸 )
38		wrdf	⊢ ( 𝐹 ∈ Word dom 𝐸 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )
39		simpll	⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )
40		fzossrbm1	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
41	25 40	syl	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
42	41	adantl	⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
43	42	sselda	⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
44	39 43	ffvelcdmd	⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐸 )
45	44	exp31	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐸 ) ) )
46	38 45	syl	⊢ ( 𝐹 ∈ Word dom 𝐸 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐸 ) ) )
47	46	adantl	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐸 ) ) )
48	47	imp	⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐸 ) )
49	48	ad3antrrr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐸 ) )
50	49	imp	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐸 )
51	37 50	ffvelcdmd	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ran 𝐸 )
52		eqcom	⊢ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) )
53	52	biimpi	⊢ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) )
54	53	eleq1d	⊢ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ran 𝐸 ) )
55	51 54	syl5ibrcom	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
56	55	ralimdva	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
57	35 56	syldc	⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
58	57	adantr	⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
59	58	impcom	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 )
60		breq2	⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) ↔ 2 ≤ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
61	60	adantl	⊢ ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) ↔ 2 ≤ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
62		2re	⊢ 2 ∈ ℝ
63	62	a1i	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 2 ∈ ℝ )
64		1red	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 1 ∈ ℝ )
65	63 64 28	lesubaddd	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 2 − 1 ) ≤ ( ♯ ‘ 𝐹 ) ↔ 2 ≤ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
66		2m1e1	⊢ ( 2 − 1 ) = 1
67	66	breq1i	⊢ ( ( 2 − 1 ) ≤ ( ♯ ‘ 𝐹 ) ↔ 1 ≤ ( ♯ ‘ 𝐹 ) )
68		elnnnn0c	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) )
69	68	simplbi2	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 1 ≤ ( ♯ ‘ 𝐹 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
70	67 69	biimtrid	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 2 − 1 ) ≤ ( ♯ ‘ 𝐹 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
71	65 70	sylbird	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 2 ≤ ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
72	71	adantl	⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 2 ≤ ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
73	72	adantr	⊢ ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( 2 ≤ ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
74	61 73	sylbid	⊢ ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
75	74	imp	⊢ ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
76	75	adantr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
77		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ )
78	76 77	sylibr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
79		fzoend	⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
80	78 79	syl	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
81		2fveq3	⊢ ( 𝑖 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
82		fveq2	⊢ ( 𝑖 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
83		fvoveq1	⊢ ( 𝑖 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) )
84	82 83	preq12d	⊢ ( 𝑖 = ( ( ♯ ‘ 𝐹 ) − 1 ) → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } )
85	81 84	eqeq12d	⊢ ( 𝑖 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ) )
86	85	adantl	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ 𝑖 = ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ) )
87	80 86	rspcdv	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ) )
88	14 15	npcand	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
89	88	ad4antlr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
90	89	fveq2d	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
91	90	preq2d	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } )
92	91	eqeq2d	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ↔ ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) )
93	38	ad4antlr	⊢ ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )
94	71	com12	⊢ ( 2 ≤ ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
95	60 94	syl6bi	⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
96	95	com3r	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
97	96	adantl	⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
98	97	imp31	⊢ ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
99	98 77	sylibr	⊢ ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
100	99 79	syl	⊢ ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
101	93 100	ffvelcdmd	⊢ ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ dom 𝐸 )
102	101	adantr	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ dom 𝐸 )
103	36 102	ffvelcdmd	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ ran 𝐸 )
104		eqcom	⊢ ( ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } = ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
105	104	biimpi	⊢ ( ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } = ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
106	105	eleq1d	⊢ ( ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ↔ ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ ran 𝐸 ) )
107	103 106	syl5ibrcom	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ) )
108	92 107	sylbid	⊢ ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → ( ( 𝐸 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ) )
109	87 108	syldc	⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ) )
110	109	adantr	⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ) )
111	110	impcom	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 )
112		preq2	⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } )
113	112	eleq1d	⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ) )
114	113	adantl	⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ) )
115	114	adantl	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∈ ran 𝐸 ) )
116	111 115	mpbird	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 )
117	24 59 116	3jca	⊢ ( ( ( ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐸 : dom 𝐸 ⟶ ran 𝐸 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
118	117	exp41	⊢ ( ( ( ( 𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) )
119	118	exp41	⊢ ( 𝑃 ∈ Word 𝑉 → ( 𝐹 ∈ Word dom 𝐸 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) ) ) )
120	8 119	syl	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝐹 ∈ Word dom 𝐸 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) ) ) )
121	120	com13	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝐹 ∈ Word dom 𝐸 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) ) ) )
122	4 121	mpcom	⊢ ( 𝐹 ∈ Word dom 𝐸 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) ) )
123	122	imp	⊢ ( ( 𝐹 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) )
124	7 123	mpd	⊢ ( ( 𝐹 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) )
125	124	expcom	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝐹 ∈ Word dom 𝐸 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) )
126	125	com14	⊢ ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 → ( 𝐹 ∈ Word dom 𝐸 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) )
127	126	imp	⊢ ( ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) )
128	127	impcomd	⊢ ( ( 𝐸 : dom 𝐸 ⟶ ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸 ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
129	3 128	sylan	⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝐹 ∈ Word dom 𝐸 ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
130	129	3imp	⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )