Metamath Proof Explorer


Theorem clwwlknonex2

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 28-Mar-2022)

Ref Expression
Hypotheses clwwlknonex2.v 𝑉 = ( Vtx ‘ 𝐺 )
clwwlknonex2.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion clwwlknonex2 ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v 𝑉 = ( Vtx ‘ 𝐺 )
2 clwwlknonex2.e 𝐸 = ( Edg ‘ 𝐺 )
3 uz3m2nn ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
4 3 nnne0d ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( 𝑁 − 2 ) ≠ 0 )
5 4 3ad2ant3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑁 − 2 ) ≠ 0 )
6 1 2 clwwlknonel ( ( 𝑁 − 2 ) ≠ 0 → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
7 5 6 syl ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
8 simpr11 ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → 𝑊 ∈ Word 𝑉 )
9 8 adantr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 𝑊 ∈ Word 𝑉 )
10 simpll1 ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 𝑋𝑉 )
11 simpll2 ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 𝑌𝑉 )
12 ccatw2s1cl ( ( 𝑊 ∈ Word 𝑉𝑋𝑉𝑌𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 )
13 9 10 11 12 syl3anc ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 )
14 1 2 clwwlknonex2lem2 ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
15 simp11 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → 𝑊 ∈ Word 𝑉 )
16 15 ad2antlr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 𝑊 ∈ Word 𝑉 )
17 ccatw2s1len ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
18 16 17 syl ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
19 18 oveq1d ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) )
20 19 oveq2d ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) ) )
21 simp3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑁 ∈ ( ℤ ‘ 3 ) )
22 simp2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) )
23 21 22 anim12i ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) )
24 23 adantr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) )
25 clwwlknonex2lem1 ( ( 𝑁 ∈ ( ℤ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) )
26 24 25 syl ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) )
27 20 26 eqtrd ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) )
28 27 raleqdv ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
29 14 28 mpbird ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
30 ccatws1cl ( ( 𝑊 ∈ Word 𝑉𝑋𝑉 ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 )
31 lswccats1 ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉𝑌𝑉 ) → ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑌 )
32 30 31 stoic3 ( ( 𝑊 ∈ Word 𝑉𝑋𝑉𝑌𝑉 ) → ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑌 )
33 16 10 11 32 syl3anc ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑌 )
34 3 nngt0d ( 𝑁 ∈ ( ℤ ‘ 3 ) → 0 < ( 𝑁 − 2 ) )
35 breq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 2 ) ) )
36 34 35 syl5ibr ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
37 36 3ad2ant2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
38 37 com12 ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
39 38 3ad2ant3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
40 39 imp ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
41 40 adantr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 0 < ( ♯ ‘ 𝑊 ) )
42 ccat2s1fst ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
43 16 41 42 syl2anc ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
44 33 43 preq12d ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } = { 𝑌 , ( 𝑊 ‘ 0 ) } )
45 prcom { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
46 45 eleq1i ( { 𝑋 , 𝑌 } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 )
47 46 biimpi ( { 𝑋 , 𝑌 } ∈ 𝐸 → { 𝑌 , 𝑋 } ∈ 𝐸 )
48 47 adantl ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { 𝑌 , 𝑋 } ∈ 𝐸 )
49 preq2 ( ( 𝑊 ‘ 0 ) = 𝑋 → { 𝑌 , ( 𝑊 ‘ 0 ) } = { 𝑌 , 𝑋 } )
50 49 eleq1d ( ( 𝑊 ‘ 0 ) = 𝑋 → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
51 50 3ad2ant3 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
52 51 ad2antlr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
53 48 52 mpbird ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 )
54 44 53 eqeltrd ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 )
55 13 29 54 3jca ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
56 17 3ad2ant1 ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
57 56 3ad2ant1 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
58 57 ad2antlr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
59 oveq1 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = ( ( 𝑁 − 2 ) + 2 ) )
60 eluzelcn ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℂ )
61 2cn 2 ∈ ℂ
62 npcan ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
63 60 61 62 sylancl ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
64 59 63 sylan9eq ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ 𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
65 64 ex ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
66 65 3ad2ant2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
67 66 com12 ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
68 67 3ad2ant3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
69 68 imp ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
70 69 adantr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
71 58 70 eqtrd ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 )
72 55 71 jca ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) )
73 72 exp31 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
74 7 73 sylbid ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
75 74 com23 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
76 75 3imp ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) )
77 eluzge3nn ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℕ )
78 1 2 isclwwlknx ( 𝑁 ∈ ℕ → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
79 77 78 syl ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
80 79 3ad2ant3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
81 80 3ad2ant1 ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
82 76 81 mpbird ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )