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 bilani ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { 𝑌 , 𝑋 } ∈ 𝐸 )
47 preq2 ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → { 𝑌 , ( 𝑊 ‘ 0 ) } = { 𝑌 , 𝑋 } )
48 47 eleq1d ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
49 48 3ad2ant3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
50 49 ad2antlr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { 𝑌 , 𝑋 } ∈ 𝐸 ) )
51 46 50 mpbird ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { 𝑌 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 )
52 43 51 eqeltrd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 )
53 13 28 52 3jca ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
54 17 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
55 54 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
56 55 ad2antlr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
57 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = ( ( 𝑁 − 2 ) + 2 ) )
58 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℂ )
59 2cn ⊢ 2 ∈ ℂ
60 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
61 58 59 60 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
62 57 61 sylan9eq ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
63 62 ex ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
64 63 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
65 64 com12 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
66 65 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 ) )
67 66 imp ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
68 67 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) + 2 ) = 𝑁 )
69 56 68 eqtrd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 )
70 53 69 jca ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) )
71 70 exp31 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
72 7 71 sylbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
73 72 com23 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) ) )
74 73 3imp ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) )
75 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
76 1 2 isclwwlknx ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
77 75 76 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
78 77 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
79 78 3ad2ant1 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) − 1 ) ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = 𝑁 ) ) )
80 74 79 mpbird ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )