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

Metamath Proof Explorer

Theorem clwwlkf1

Description: Lemma 3 for clwwlkf1o : F is a 1-1 function. (Contributed by AV, 28-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwwlkf1o.d ⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
clwwlkf1o.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
Assertion clwwlkf1 ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 –1-1→ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d ⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
2 clwwlkf1o.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
3 1 2 clwwlkf ⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 ⟶ ( 𝑁 ClWWalksN 𝐺 ) )
4 1 2 clwwlkfv ⊢ ( 𝑥 ∈ 𝐷 → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 prefix 𝑁 ) )
5 1 2 clwwlkfv ⊢ ( 𝑦 ∈ 𝐷 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 prefix 𝑁 ) )
6 4 5 eqeqan12d ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) )
7 6 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) )
8 fveq2 ⊢ ( 𝑤 = 𝑥 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑥 ) )
9 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 0 ) = ( 𝑥 ‘ 0 ) )
10 8 9 eqeq12d ⊢ ( 𝑤 = 𝑥 → ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ↔ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) )
11 10 1 elrab2 ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) )
12 fveq2 ⊢ ( 𝑤 = 𝑦 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑦 ) )
13 fveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
14 12 13 eqeq12d ⊢ ( 𝑤 = 𝑦 → ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ↔ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) )
15 14 1 elrab2 ⊢ ( 𝑦 ∈ 𝐷 ↔ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) )
16 11 15 anbi12i ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ↔ ( ( 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ∧ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ) )
17 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
18 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
19 17 18 wwlknp ⊢ ( 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑥 ‘ 𝑖 ) , ( 𝑥 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
20 17 18 wwlknp ⊢ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
21 simprlr ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) )
22 simpllr ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) )
23 21 22 eqtr4d ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
24 23 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
25 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
26 ax-1cn ⊢ 1 ∈ ℂ
27 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
28 27 eqcomd ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → 𝑁 = ( ( 𝑁 + 1 ) − 1 ) )
29 25 26 28 sylancl ⊢ ( 𝑁 ∈ ℕ → 𝑁 = ( ( 𝑁 + 1 ) − 1 ) )
30 oveq1 ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑥 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
31 30 eqcomd ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) → ( ( 𝑁 + 1 ) − 1 ) = ( ( ♯ ‘ 𝑥 ) − 1 ) )
32 29 31 sylan9eqr ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 = ( ( ♯ ‘ 𝑥 ) − 1 ) )
33 32 oveq2d ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑥 prefix 𝑁 ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
34 32 oveq2d ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑦 prefix 𝑁 ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
35 33 34 eqeq12d ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) )
36 35 ex ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) ) )
37 36 ad2antlr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) ) )
38 37 adantl ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) ) )
39 38 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) )
40 39 biimpa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
41 simpll ⊢ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
42 simpll ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) )
43 41 42 anim12ci ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) )
44 43 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) )
45 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
46 0nn0 ⊢ 0 ∈ ℕ0
47 45 46 jctil ⊢ ( 𝑁 ∈ ℕ → ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
48 47 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
49 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
50 49 lep1d ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≤ ( 𝑁 + 1 ) )
51 breq2 ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) → ( 𝑁 ≤ ( ♯ ‘ 𝑥 ) ↔ 𝑁 ≤ ( 𝑁 + 1 ) ) )
52 50 51 imbitrrid ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑁 ≤ ( ♯ ‘ 𝑥 ) ) )
53 52 ad2antlr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → 𝑁 ≤ ( ♯ ‘ 𝑥 ) ) )
54 53 adantl ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( 𝑁 ∈ ℕ → 𝑁 ≤ ( ♯ ‘ 𝑥 ) ) )
55 54 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → 𝑁 ≤ ( ♯ ‘ 𝑥 ) )
56 breq2 ⊢ ( ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) → ( 𝑁 ≤ ( ♯ ‘ 𝑦 ) ↔ 𝑁 ≤ ( 𝑁 + 1 ) ) )
57 50 56 imbitrrid ⊢ ( ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑁 ≤ ( ♯ ‘ 𝑦 ) ) )
58 57 ad2antlr ⊢ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → 𝑁 ≤ ( ♯ ‘ 𝑦 ) ) )
59 58 adantr ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( 𝑁 ∈ ℕ → 𝑁 ≤ ( ♯ ‘ 𝑦 ) ) )
60 59 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → 𝑁 ≤ ( ♯ ‘ 𝑦 ) )
61 pfxval ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 prefix 𝑁 ) = ( 𝑥 substr ⟨ 0 , 𝑁 ⟩ ) )
62 61 ad2ant2rl ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑥 prefix 𝑁 ) = ( 𝑥 substr ⟨ 0 , 𝑁 ⟩ ) )
63 pfxval ⊢ ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑦 prefix 𝑁 ) = ( 𝑦 substr ⟨ 0 , 𝑁 ⟩ ) )
64 63 ad2ant2l ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑦 prefix 𝑁 ) = ( 𝑦 substr ⟨ 0 , 𝑁 ⟩ ) )
65 62 64 eqeq12d ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ( 𝑥 substr ⟨ 0 , 𝑁 ⟩ ) = ( 𝑦 substr ⟨ 0 , 𝑁 ⟩ ) ) )
66 65 3adant3 ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑥 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ( 𝑥 substr ⟨ 0 , 𝑁 ⟩ ) = ( 𝑦 substr ⟨ 0 , 𝑁 ⟩ ) ) )
67 swrdspsleq ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑥 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑥 substr ⟨ 0 , 𝑁 ⟩ ) = ( 𝑦 substr ⟨ 0 , 𝑁 ⟩ ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) )
68 66 67 bitrd ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑥 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) )
69 44 48 55 60 68 syl112anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) )
70 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
71 70 biimpri ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ..^ 𝑁 ) )
72 71 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → 0 ∈ ( 0 ..^ 𝑁 ) )
73 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑥 ‘ 𝑖 ) = ( 𝑥 ‘ 0 ) )
74 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑦 ‘ 𝑖 ) = ( 𝑦 ‘ 0 ) )
75 73 74 eqeq12d ⊢ ( 𝑖 = 0 → ( ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
76 75 rspcv ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
77 72 76 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
78 69 77 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
79 78 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
80 simpr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) )
81 simpr ⊢ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) )
82 80 81 eqeqan12rd ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑦 ) ↔ ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
83 82 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑦 ) ↔ ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
84 79 83 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑦 ) )
85 24 40 84 jca32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑦 ) ) ) )
86 42 adantl ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) )
87 86 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) )
88 41 adantr ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
89 88 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
90 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
91 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
92 0lt1 ⊢ 0 < 1
93 92 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
94 49 90 91 93 addgt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 + 1 ) )
95 breq2 ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) → ( 0 < ( ♯ ‘ 𝑥 ) ↔ 0 < ( 𝑁 + 1 ) ) )
96 94 95 imbitrrid ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 0 < ( ♯ ‘ 𝑥 ) ) )
97 96 ad2antlr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → 0 < ( ♯ ‘ 𝑥 ) ) )
98 97 adantl ⊢ ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( 𝑁 ∈ ℕ → 0 < ( ♯ ‘ 𝑥 ) ) )
99 98 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → 0 < ( ♯ ‘ 𝑥 ) )
100 87 89 99 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 < ( ♯ ‘ 𝑥 ) ) )
101 100 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 < ( ♯ ‘ 𝑥 ) ) )
102 pfxsuff1eqwrdeq ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 < ( ♯ ‘ 𝑥 ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑦 ) ) ) ) )
103 101 102 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) = ( 𝑦 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑦 ) ) ) ) )
104 85 103 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) ) ∧ ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) ) → 𝑥 = 𝑦 )
105 104 exp31 ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ∧ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) )
106 105 expdcom ⊢ ( ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) )
107 106 ex ⊢ ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) → ( ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) → ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) ) )
108 107 3adant3 ⊢ ( ( 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) → ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) ) )
109 20 108 syl ⊢ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) → ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) ) )
110 109 imp ⊢ ( ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) )
111 110 expdcom ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ) → ( ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) → ( ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) ) )
112 111 3adant3 ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑥 ‘ 𝑖 ) , ( 𝑥 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) → ( ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) ) )
113 19 112 syl ⊢ ( 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) → ( ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) ) ) )
114 113 imp31 ⊢ ( ( ( 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ∧ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) )
115 114 com12 ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ) ∧ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑦 ) = ( 𝑦 ‘ 0 ) ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) )
116 16 115 biimtrid ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) ) )
117 116 imp ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( ( 𝑥 prefix 𝑁 ) = ( 𝑦 prefix 𝑁 ) → 𝑥 = 𝑦 ) )
118 7 117 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
119 118 ralrimivva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
120 dff13 ⊢ ( 𝐹 : 𝐷 –1-1→ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝐹 : 𝐷 ⟶ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
121 3 119 120 sylanbrc ⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 –1-1→ ( 𝑁 ClWWalksN 𝐺 ) )