Metamath Proof Explorer

Theorem clwlkclwwlklem1

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

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

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ V
2 mptexg ⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ V → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ V )
3 1 2 mp1i ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ V )
4 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
5 4 clwlkclwwlklem2a ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ) ) )
6 5 adantr ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ) ) )
7 eleq1 ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( 𝑓 ∈ Word dom 𝐸 ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ Word dom 𝐸 ) )
8 fveq2 ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) )
9 8 oveq2d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) )
10 9 feq2d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ⟶ 𝑉 ) )
11 8 oveq2d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) )
12 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( 𝑓 ‘ 𝑖 ) = ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) )
13 12 fveqeq2d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
14 11 13 raleqbidv ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
15 7 10 14 3anbi123d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
16 2fveq3 ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑃 ‘ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) )
17 16 eqeq2d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ) )
18 15 17 anbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ) ) )
19 18 imbi2d ⊢ ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) → ( ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) ↔ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ) ) ) )
20 19 adantl ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) → ( ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) ↔ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ( 𝐸 ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) ) ) ) ) )
21 6 20 mpbird ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
22 3 21 spcimedv ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )