Metamath Proof Explorer

Theorem wwlksnextinj

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wwlksnextbij0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
wwlksnextbij0.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
wwlksnextbij0.r ⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
wwlksnextbij0.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
Assertion wwlksnextinj ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 –1-1→ 𝑅 )

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlksnextbij0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 wwlksnextbij0.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
4 wwlksnextbij0.r ⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
5 wwlksnextbij0.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
6 1 2 3 4 5 wwlksnextfun ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 ⟶ 𝑅 )
7 fveq2 ⊢ ( 𝑡 = 𝑑 → ( lastS ‘ 𝑡 ) = ( lastS ‘ 𝑑 ) )
8 fvex ⊢ ( lastS ‘ 𝑑 ) ∈ V
9 7 5 8 fvmpt ⊢ ( 𝑑 ∈ 𝐷 → ( 𝐹 ‘ 𝑑 ) = ( lastS ‘ 𝑑 ) )
10 fveq2 ⊢ ( 𝑡 = 𝑥 → ( lastS ‘ 𝑡 ) = ( lastS ‘ 𝑥 ) )
11 fvex ⊢ ( lastS ‘ 𝑥 ) ∈ V
12 10 5 11 fvmpt ⊢ ( 𝑥 ∈ 𝐷 → ( 𝐹 ‘ 𝑥 ) = ( lastS ‘ 𝑥 ) )
13 9 12 eqeqan12d ⊢ ( ( 𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) )
15 fveqeq2 ⊢ ( 𝑤 = 𝑑 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ↔ ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ) )
16 oveq1 ⊢ ( 𝑤 = 𝑑 → ( 𝑤 prefix ( 𝑁 + 1 ) ) = ( 𝑑 prefix ( 𝑁 + 1 ) ) )
17 16 eqeq1d ⊢ ( 𝑤 = 𝑑 → ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
18 fveq2 ⊢ ( 𝑤 = 𝑑 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑑 ) )
19 18 preq2d ⊢ ( 𝑤 = 𝑑 → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } )
20 19 eleq1d ⊢ ( 𝑤 = 𝑑 → ( { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) )
21 15 17 20 3anbi123d ⊢ ( 𝑤 = 𝑑 → ( ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) )
22 21 3 elrab2 ⊢ ( 𝑑 ∈ 𝐷 ↔ ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) )
23 fveqeq2 ⊢ ( 𝑤 = 𝑥 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ↔ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ) )
24 oveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
25 24 eqeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
26 fveq2 ⊢ ( 𝑤 = 𝑥 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑥 ) )
27 26 preq2d ⊢ ( 𝑤 = 𝑥 → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } )
28 27 eleq1d ⊢ ( 𝑤 = 𝑥 → ( { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) )
29 23 25 28 3anbi123d ⊢ ( 𝑤 = 𝑥 → ( ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) )
30 29 3 elrab2 ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) )
31 eqtr3 ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) )
32 31 expcom ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ) )
33 32 3ad2ant1 ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ) )
34 33 adantl ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ) )
35 34 com12 ⊢ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ) )
36 35 3ad2ant1 ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ) )
37 36 adantl ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ) )
38 37 imp ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) )
39 38 adantr ⊢ ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) )
40 39 adantr ⊢ ( ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) )
41 simpr ⊢ ( ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) → ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) )
42 eqtr3 ⊢ ( ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ) → ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
43 1e2m1 ⊢ 1 = ( 2 − 1 )
44 43 a1i ⊢ ( 𝑁 ∈ ℕ0 → 1 = ( 2 − 1 ) )
45 44 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) = ( 𝑁 + ( 2 − 1 ) ) )
46 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
47 2cnd ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
48 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
49 46 47 48 addsubassd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 2 ) − 1 ) = ( 𝑁 + ( 2 − 1 ) ) )
50 45 49 eqtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) = ( ( 𝑁 + 2 ) − 1 ) )
51 50 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ) → ( 𝑁 + 1 ) = ( ( 𝑁 + 2 ) − 1 ) )
52 oveq1 ⊢ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ( ♯ ‘ 𝑑 ) − 1 ) = ( ( 𝑁 + 2 ) − 1 ) )
53 52 eqeq2d ⊢ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑑 ) − 1 ) ↔ ( 𝑁 + 1 ) = ( ( 𝑁 + 2 ) − 1 ) ) )
54 53 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ) → ( ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑑 ) − 1 ) ↔ ( 𝑁 + 1 ) = ( ( 𝑁 + 2 ) − 1 ) ) )
55 51 54 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ) → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑑 ) − 1 ) )
56 oveq2 ⊢ ( ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑑 ) − 1 ) → ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
57 oveq2 ⊢ ( ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑑 ) − 1 ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
58 56 57 eqeq12d ⊢ ( ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑑 ) − 1 ) → ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ↔ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) )
59 55 58 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ) → ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ↔ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) )
60 59 biimpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ) → ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) )
61 60 ex ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
62 61 com13 ⊢ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
63 42 62 syl ⊢ ( ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ) → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
64 63 ex ⊢ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) ) )
65 64 com23 ⊢ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) ) )
66 65 impcom ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
67 66 com12 ⊢ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
68 67 3ad2ant2 ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
69 68 adantl ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
70 69 com12 ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ) → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
71 70 3adant3 ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
72 71 adantl ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
73 72 imp31 ⊢ ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
74 73 adantr ⊢ ( ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) → ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
75 simpl ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) → 𝑑 ∈ Word 𝑉 )
76 simpl ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → 𝑥 ∈ Word 𝑉 )
77 75 76 anim12i ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) → ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) )
78 77 adantr ⊢ ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) )
79 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
80 2re ⊢ 2 ∈ ℝ
81 80 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
82 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
83 2pos ⊢ 0 < 2
84 83 a1i ⊢ ( 𝑁 ∈ ℕ0 → 0 < 2 )
85 79 81 82 84 addgegt0d ⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 2 ) )
86 85 adantl ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) → 0 < ( 𝑁 + 2 ) )
87 breq2 ⊢ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( 0 < ( ♯ ‘ 𝑑 ) ↔ 0 < ( 𝑁 + 2 ) ) )
88 87 adantr ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 < ( ♯ ‘ 𝑑 ) ↔ 0 < ( 𝑁 + 2 ) ) )
89 86 88 mpbird ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) → 0 < ( ♯ ‘ 𝑑 ) )
90 hashgt0n0 ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑑 ) ) → 𝑑 ≠ ∅ )
91 89 90 sylan2 ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) ) → 𝑑 ≠ ∅ )
92 91 exp32 ⊢ ( 𝑑 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( 𝑁 ∈ ℕ0 → 𝑑 ≠ ∅ ) ) )
93 92 com12 ⊢ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) → ( 𝑑 ∈ Word 𝑉 → ( 𝑁 ∈ ℕ0 → 𝑑 ≠ ∅ ) ) )
94 93 3ad2ant1 ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) → ( 𝑑 ∈ Word 𝑉 → ( 𝑁 ∈ ℕ0 → 𝑑 ≠ ∅ ) ) )
95 94 impcom ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) → ( 𝑁 ∈ ℕ0 → 𝑑 ≠ ∅ ) )
96 95 adantr ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) → ( 𝑁 ∈ ℕ0 → 𝑑 ≠ ∅ ) )
97 96 imp ⊢ ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑑 ≠ ∅ )
98 85 adantl ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) → 0 < ( 𝑁 + 2 ) )
99 breq2 ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) → ( 0 < ( ♯ ‘ 𝑥 ) ↔ 0 < ( 𝑁 + 2 ) ) )
100 99 adantr ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 < ( ♯ ‘ 𝑥 ) ↔ 0 < ( 𝑁 + 2 ) ) )
101 98 100 mpbird ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) → 0 < ( ♯ ‘ 𝑥 ) )
102 hashgt0n0 ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑥 ) ) → 𝑥 ≠ ∅ )
103 101 102 sylan2 ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑁 ∈ ℕ0 ) ) → 𝑥 ≠ ∅ )
104 103 exp32 ⊢ ( 𝑥 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) → ( 𝑁 ∈ ℕ0 → 𝑥 ≠ ∅ ) ) )
105 104 com12 ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) → ( 𝑥 ∈ Word 𝑉 → ( 𝑁 ∈ ℕ0 → 𝑥 ≠ ∅ ) ) )
106 105 3ad2ant1 ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 ∈ Word 𝑉 → ( 𝑁 ∈ ℕ0 → 𝑥 ≠ ∅ ) ) )
107 106 impcom ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) → ( 𝑁 ∈ ℕ0 → 𝑥 ≠ ∅ ) )
108 107 adantl ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) → ( 𝑁 ∈ ℕ0 → 𝑥 ≠ ∅ ) )
109 108 imp ⊢ ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑥 ≠ ∅ )
110 78 97 109 jca32 ⊢ ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) ) )
111 110 adantr ⊢ ( ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) → ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) ) )
112 simpl ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) → 𝑑 ∈ Word 𝑉 )
113 112 adantr ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) ) → 𝑑 ∈ Word 𝑉 )
114 simpr ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) → 𝑥 ∈ Word 𝑉 )
115 114 adantr ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ Word 𝑉 )
116 hashneq0 ⊢ ( 𝑑 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑑 ) ↔ 𝑑 ≠ ∅ ) )
117 116 biimprd ⊢ ( 𝑑 ∈ Word 𝑉 → ( 𝑑 ≠ ∅ → 0 < ( ♯ ‘ 𝑑 ) ) )
118 117 adantr ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑑 ≠ ∅ → 0 < ( ♯ ‘ 𝑑 ) ) )
119 118 com12 ⊢ ( 𝑑 ≠ ∅ → ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) → 0 < ( ♯ ‘ 𝑑 ) ) )
120 119 adantr ⊢ ( ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) → ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) → 0 < ( ♯ ‘ 𝑑 ) ) )
121 120 impcom ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) ) → 0 < ( ♯ ‘ 𝑑 ) )
122 pfxsuff1eqwrdeq ⊢ ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑑 ) ) → ( 𝑑 = 𝑥 ↔ ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) ) ) )
123 113 115 121 122 syl3anc ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) ) → ( 𝑑 = 𝑥 ↔ ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) ) ) )
124 ancom ⊢ ( ( ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) ↔ ( ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ∧ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) )
125 124 anbi2i ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) ) ↔ ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ∧ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
126 3anass ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ∧ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ↔ ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ∧ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
127 125 126 bitr4i ⊢ ( ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) ) ↔ ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ∧ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) )
128 123 127 bitrdi ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅ ) ) → ( 𝑑 = 𝑥 ↔ ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ∧ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
129 111 128 syl ⊢ ( ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) → ( 𝑑 = 𝑥 ↔ ( ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑥 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ∧ ( 𝑑 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑥 prefix ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) ) )
130 40 41 74 129 mpbir3and ⊢ ( ( ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) ) → 𝑑 = 𝑥 )
131 130 exp31 ⊢ ( ( ( 𝑑 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑑 ) = ( 𝑁 + 2 ) ∧ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) ) → ( 𝑁 ∈ ℕ0 → ( ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) → 𝑑 = 𝑥 ) ) )
132 22 30 131 syl2anb ⊢ ( ( 𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑁 ∈ ℕ0 → ( ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) → 𝑑 = 𝑥 ) ) )
133 132 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) ) → ( ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑥 ) → 𝑑 = 𝑥 ) )
134 14 133 sylbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝑥 ) → 𝑑 = 𝑥 ) )
135 134 ralrimivva ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑑 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝑥 ) → 𝑑 = 𝑥 ) )
136 dff13 ⊢ ( 𝐹 : 𝐷 –1-1→ 𝑅 ↔ ( 𝐹 : 𝐷 ⟶ 𝑅 ∧ ∀ 𝑑 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝑥 ) → 𝑑 = 𝑥 ) ) )
137 6 135 136 sylanbrc ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 –1-1→ 𝑅 )