This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwlkccatlem

Description: Lemma for clwwlkccat : index j is shifted up by ( #A ) , and the case i = ( ( #A ) - 1 ) is covered by the "bridge" { ( lastSA ) , ( B0 ) } = { ( lastSA ) , ( A0 ) } e. ( EdgG ) . (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion clwwlkccatlem ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) )
2 simplr ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
3 lencl ⊢ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
4 3 nn0zd ⊢ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
5 fzossrbm1 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
6 4 5 syl ⊢ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
7 6 ad2antrr ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
8 7 sselda ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
9 ccatval1 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
10 1 2 8 9 syl3anc ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
11 4 ad2antrr ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
12 elfzom1elp1fzo ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
13 11 12 sylan ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
14 ccatval1 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ( 𝐴 ‘ ( 𝑖 + 1 ) ) )
15 1 2 13 14 syl3anc ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ( 𝐴 ‘ ( 𝑖 + 1 ) ) )
16 10 15 preq12d ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } )
17 16 eleq1d ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
18 17 biimprd ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
19 18 ralimdva ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
20 19 impancom ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
21 20 3adant3 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
22 21 com12 ⊢ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
23 22 adantr ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
24 23 3ad2ant1 ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
25 24 impcom ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
26 25 3adant3 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
27 simprl ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) )
28 simpll ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
29 simprr ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → 𝐴 ≠ ∅ )
30 ccatval1lsw ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( lastS ‘ 𝐴 ) )
31 27 28 29 30 syl3anc ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( lastS ‘ 𝐴 ) )
32 31 adantr ⊢ ( ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( lastS ‘ 𝐴 ) )
33 3 nn0cnd ⊢ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
34 npcan1 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐴 ) )
35 33 34 syl ⊢ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐴 ) )
36 35 ad2antrl ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐴 ) )
37 36 fveq2d ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( ♯ ‘ 𝐴 ) ) )
38 simplr ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → 𝐵 ≠ ∅ )
39 ccatval21sw ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) )
40 27 28 38 39 syl3anc ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) )
41 37 40 eqtrd ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) = ( 𝐵 ‘ 0 ) )
42 41 adantr ⊢ ( ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) = ( 𝐵 ‘ 0 ) )
43 simpr ⊢ ( ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
44 42 43 eqtr4d ⊢ ( ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) = ( 𝐴 ‘ 0 ) )
45 32 44 preq12d ⊢ ( ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } = { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } )
46 45 eleq1d ⊢ ( ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
47 46 exbiri ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ( { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
48 47 com23 ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ) → ( { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
49 48 expimpd ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
50 49 3ad2ant1 ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
51 50 com12 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
52 51 3adant2 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
53 52 3imp ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
54 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝐴 ) − 1 ) } { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
55 ovex ⊢ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ V
56 fveq2 ⊢ ( 𝑖 = ( ( ♯ ‘ 𝐴 ) − 1 ) → ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
57 fvoveq1 ⊢ ( 𝑖 = ( ( ♯ ‘ 𝐴 ) − 1 ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) )
58 56 57 preq12d ⊢ ( 𝑖 = ( ( ♯ ‘ 𝐴 ) − 1 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } )
59 58 eleq1d ⊢ ( 𝑖 = ( ( ♯ ‘ 𝐴 ) − 1 ) → ( { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
60 55 59 ralsn ⊢ ( ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝐴 ) − 1 ) } { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
61 60 anbi2i ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝐴 ) − 1 ) } { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
62 54 61 bitri ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
63 26 53 62 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
64 0z ⊢ 0 ∈ ℤ
65 lennncl ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
66 0p1e1 ⊢ ( 0 + 1 ) = 1
67 66 fveq2i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
68 67 eleq2i ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ↔ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
69 elnnuz ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
70 68 69 bitr4i ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ )
71 65 70 sylibr ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
72 fzosplitsnm1 ⊢ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) )
73 64 71 72 sylancr ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) )
74 73 raleqdv ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
75 74 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
76 75 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝐴 ) − 1 ) } ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
77 63 76 mpbird ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
78 lencl ⊢ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
79 78 nn0zd ⊢ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
80 peano2zm ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ )
81 79 80 syl ⊢ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ )
82 81 ad2antrl ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ )
83 82 adantr ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ )
84 83 anim1ci ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ ) )
85 fzosubel3 ⊢ ( ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ ) → ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
86 fveq2 ⊢ ( 𝑗 = ( 𝑖 − ( ♯ ‘ 𝐴 ) ) → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) )
87 fvoveq1 ⊢ ( 𝑗 = ( 𝑖 − ( ♯ ‘ 𝐴 ) ) → ( 𝐵 ‘ ( 𝑗 + 1 ) ) = ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) )
88 86 87 preq12d ⊢ ( 𝑗 = ( 𝑖 − ( ♯ ‘ 𝐴 ) ) → { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } = { ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) } )
89 88 eleq1d ⊢ ( 𝑗 = ( 𝑖 − ( ♯ ‘ 𝐴 ) ) → ( { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
90 89 rspcv ⊢ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
91 84 85 90 3syl ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
92 simp-4l ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) )
93 simprl ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
94 93 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
95 3 adantr ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
96 78 adantr ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
97 nn0addcl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
98 97 nn0zd ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
99 95 96 98 syl2an ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
100 1nn0 ⊢ 1 ∈ ℕ0
101 eluzmn ⊢ ( ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 1 ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) )
102 99 100 101 sylancl ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) )
103 33 ad2antrr ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
104 78 nn0cnd ⊢ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
105 104 ad2antrl ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
106 1cnd ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → 1 ∈ ℂ )
107 103 105 106 addsubassd ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) = ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
108 107 fveq2d ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) = ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
109 102 108 eleqtrd ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
110 fzoss2 ⊢ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ⊆ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
111 109 110 syl ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ⊆ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
112 111 adantr ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ⊆ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
113 112 sselda ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
114 ccatval2 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) = ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) )
115 92 94 113 114 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) = ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) )
116 107 oveq2d ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐴 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) = ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
117 116 eleq2d ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ↔ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
118 117 adantr ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ↔ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
119 eluzmn ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ 1 ∈ ℕ0 ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
120 4 100 119 sylancl ⊢ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
121 120 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
122 fzoss1 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) → ( ( ♯ ‘ 𝐴 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ⊆ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) )
123 121 122 syl ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( ♯ ‘ 𝐴 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ⊆ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) )
124 123 sseld ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) → 𝑖 ∈ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ) )
125 118 124 sylbird ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑖 ∈ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ) )
126 125 imp ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → 𝑖 ∈ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) )
127 4 adantr ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
128 79 adantr ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
129 simpl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
130 zaddcl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
131 129 130 jca ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ) )
132 127 128 131 syl2an ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ) )
133 132 adantr ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ) )
134 elfzoelz ⊢ ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑖 ∈ ℤ )
135 1zzd ⊢ ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 1 ∈ ℤ )
136 134 135 jca ⊢ ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( 𝑖 ∈ ℤ ∧ 1 ∈ ℤ ) )
137 elfzomelpfzo ⊢ ( ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ) ∧ ( 𝑖 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑖 ∈ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) )
138 133 136 137 syl2an ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( 𝑖 ∈ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ..^ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) )
139 126 138 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( 𝑖 + 1 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
140 ccatval2 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑖 + 1 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ( 𝐵 ‘ ( ( 𝑖 + 1 ) − ( ♯ ‘ 𝐴 ) ) ) )
141 92 94 139 140 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ( 𝐵 ‘ ( ( 𝑖 + 1 ) − ( ♯ ‘ 𝐴 ) ) ) )
142 134 zcnd ⊢ ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑖 ∈ ℂ )
143 142 adantl ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → 𝑖 ∈ ℂ )
144 1cnd ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → 1 ∈ ℂ )
145 103 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
146 143 144 145 addsubd ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝑖 + 1 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) )
147 146 fveq2d ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( 𝐵 ‘ ( ( 𝑖 + 1 ) − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) )
148 141 147 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) )
149 115 148 preq12d ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) } )
150 149 eleq1d ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑖 − ( ♯ ‘ 𝐴 ) ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
151 91 150 sylibrd ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
152 151 impancom ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
153 152 ralrimiv ⊢ ( ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
154 153 exp31 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
155 154 expcom ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
156 155 com23 ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
157 156 com24 ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
158 157 imp ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
159 158 3adant3 ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
160 159 com12 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
161 160 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
162 161 3imp ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
163 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
164 77 162 163 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
165 ccatlen ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
166 165 oveq1d ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) = ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) )
167 166 ad2ant2r ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) = ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − 1 ) )
168 167 107 eqtrd ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) = ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
169 168 oveq2d ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
170 elnn0uz ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
171 3 170 sylib ⊢ ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
172 171 adantr ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
173 lennncl ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
174 nnm1nn0 ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ0 )
175 173 174 syl ⊢ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ0 )
176 fzoun ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ0 ) → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
177 172 175 176 syl2an ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
178 169 177 eqtrd ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
179 178 3ad2antr1 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
180 179 3ad2antl1 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
181 180 3adant3 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
182 164 181 raleqtrrdv ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )