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 14 27 raleqtrrdv ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
29 ccatws1cl ( ( 𝑊 ∈ Word 𝑉𝑋𝑉 ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 )
30 lswccats1 ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉𝑌𝑉 ) → ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑌 )
31 29 30 stoic3 ( ( 𝑊 ∈ Word 𝑉𝑋𝑉𝑌𝑉 ) → ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑌 )
32 16 10 11 31 syl3anc ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑌 )
33 3 nngt0d ( 𝑁 ∈ ( ℤ ‘ 3 ) → 0 < ( 𝑁 − 2 ) )
34 breq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 2 ) ) )
35 33 34 imbitrrid ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
36 35 3ad2ant2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
37 36 com12 ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
38 37 3ad2ant3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
39 38 imp ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
40 39 adantr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 0 < ( ♯ ‘ 𝑊 ) )
41 ccat2s1fst ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
42 16 40 41 syl2anc ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
43 32 42 preq12d ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } = { 𝑌 , ( 𝑊 ‘ 0 ) } )
44 prcom { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
45 44 eleq1i ( { 𝑋 , 𝑌 } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 )
46 45 biimpi ( { 𝑋 , 𝑌 } ∈ 𝐸 → { 𝑌 , 𝑋 } ∈ 𝐸 )
47 46 adantl ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { 𝑌 , 𝑋 } ∈ 𝐸 )
48 preq2 ( ( 𝑊 ‘ 0 ) = 𝑋 → { 𝑌 , ( 𝑊 ‘ 0 ) } = { 𝑌 , 𝑋 } )
49 48 eleq1d ( ( 𝑊 ‘ 0 ) = 𝑋 → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
50 49 3ad2ant3 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
51 50 ad2antlr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
52 47 51 mpbird ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 )
53 43 52 eqeltrd ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 )
54 13 28 53 3jca ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
55 17 3ad2ant1 ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
56 55 3ad2ant1 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
57 56 ad2antlr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
58 oveq1 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = ( ( 𝑁 − 2 ) + 2 ) )
59 eluzelcn ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℂ )
60 2cn 2 ∈ ℂ
61 npcan ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
62 59 60 61 sylancl ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
63 58 62 sylan9eq ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ 𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
64 63 ex ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
65 64 3ad2ant2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
66 65 com12 ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
67 66 3ad2ant3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
68 67 imp ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
69 68 adantr ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
70 57 69 eqtrd ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 )
71 54 70 jca ( ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) )
72 71 exp31 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
73 7 72 sylbid ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
74 73 com23 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
75 74 3imp ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) )
76 eluzge3nn ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℕ )
77 1 2 isclwwlknx ( 𝑁 ∈ ℕ → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
78 76 77 syl ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
79 78 3ad2ant3 ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
80 79 3ad2ant1 ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
81 75 80 mpbird ( ( ( 𝑋𝑉𝑌𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )