Metamath Proof Explorer

Theorem wwlksnextsurj

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 wwlksnextsurj ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐹 : 𝐷 –onto→ 𝑅 )

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 wwlknbp ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) )
7 simp2 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → 𝑁 ∈ ℕ0 )
8 1 2 3 4 5 wwlksnextfun ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 ⟶ 𝑅 )
9 6 7 8 3syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐹 : 𝐷 ⟶ 𝑅 )
10 preq2 ⊢ ( 𝑛 = 𝑟 → { ( lastS ‘ 𝑊 ) , 𝑛 } = { ( lastS ‘ 𝑊 ) , 𝑟 } )
11 10 eleq1d ⊢ ( 𝑛 = 𝑟 → ( { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) )
12 11 4 elrab2 ⊢ ( 𝑟 ∈ 𝑅 ↔ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) )
13 1 2 wwlksnext ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) )
14 13 3expb ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) )
15 s1cl ⊢ ( 𝑟 ∈ 𝑉 → ⟨“ 𝑟 ”⟩ ∈ Word 𝑉 )
16 pfxccat1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑟 ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
17 15 16 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
18 17 ex ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑟 ∈ 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 ) )
19 18 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑟 ∈ 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 ) )
20 oveq2 ⊢ ( ( 𝑁 + 1 ) = ( ♯ ‘ 𝑊 ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) )
21 20 eqcoms ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) )
22 21 eqeq1d ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 ) )
23 22 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 ) )
24 19 23 sylibrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑟 ∈ 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
25 24 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( 𝑟 ∈ 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
26 1 2 wwlknp ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
27 25 26 syl11 ⊢ ( 𝑟 ∈ 𝑉 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
28 27 adantr ⊢ ( ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
29 28 impcom ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 )
30 lswccats1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉 ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) = 𝑟 )
31 30 eqcomd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉 ) → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) )
32 31 ex ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) )
33 32 3ad2ant3 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) )
34 6 33 syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) )
35 34 imp ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑟 ∈ 𝑉 ) → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) )
36 35 preq2d ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑟 ∈ 𝑉 ) → { ( lastS ‘ 𝑊 ) , 𝑟 } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } )
37 36 eleq1d ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑟 ∈ 𝑉 ) → ( { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) )
38 37 biimpd ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑟 ∈ 𝑉 ) → ( { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 → { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) )
39 38 impr ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 )
40 14 29 39 jca32 ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) )
41 33 6 syl11 ⊢ ( 𝑟 ∈ 𝑉 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) )
42 41 adantr ⊢ ( ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) )
43 42 impcom ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) )
44 ovexd ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ V )
45 eleq1 ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
46 oveq1 ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( 𝑑 prefix ( 𝑁 + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) )
47 46 eqeq1d ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
48 fveq2 ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( lastS ‘ 𝑑 ) = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) )
49 48 preq2d ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } )
50 49 eleq1d ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) )
51 47 50 anbi12d ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) )
52 45 51 anbi12d ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ↔ ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) ) )
53 48 eqeq2d ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( 𝑟 = ( lastS ‘ 𝑑 ) ↔ 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) )
54 52 53 anbi12d ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) ) )
55 54 bicomd ⊢ ( 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) ↔ ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) ) )
56 55 adantl ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) ∧ 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) ↔ ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) ) )
57 56 biimpd ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) ∧ 𝑑 = ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) → ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) ) )
58 44 57 spcimedv ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑟 ”⟩ ) ) ) → ∃ 𝑑 ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) ) )
59 40 43 58 mp2and ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ∃ 𝑑 ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) )
60 oveq1 ⊢ ( 𝑤 = 𝑑 → ( 𝑤 prefix ( 𝑁 + 1 ) ) = ( 𝑑 prefix ( 𝑁 + 1 ) ) )
61 60 eqeq1d ⊢ ( 𝑤 = 𝑑 → ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
62 fveq2 ⊢ ( 𝑤 = 𝑑 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑑 ) )
63 62 preq2d ⊢ ( 𝑤 = 𝑑 → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } )
64 63 eleq1d ⊢ ( 𝑤 = 𝑑 → ( { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) )
65 61 64 anbi12d ⊢ ( 𝑤 = 𝑑 → ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) )
66 65 elrab ⊢ ( 𝑑 ∈ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ↔ ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) )
67 66 anbi1i ⊢ ( ( 𝑑 ∈ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) ↔ ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) )
68 67 exbii ⊢ ( ∃ 𝑑 ( 𝑑 ∈ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) ↔ ∃ 𝑑 ( ( 𝑑 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑑 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑑 ) } ∈ 𝐸 ) ) ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) )
69 59 68 sylibr ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ∃ 𝑑 ( 𝑑 ∈ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) )
70 df-rex ⊢ ( ∃ 𝑑 ∈ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } 𝑟 = ( lastS ‘ 𝑑 ) ↔ ∃ 𝑑 ( 𝑑 ∈ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ∧ 𝑟 = ( lastS ‘ 𝑑 ) ) )
71 69 70 sylibr ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ∃ 𝑑 ∈ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } 𝑟 = ( lastS ‘ 𝑑 ) )
72 1 2 3 wwlksnextwrd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐷 = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } )
73 72 adantr ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → 𝐷 = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } )
74 71 73 rexeqtrrdv ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ∃ 𝑑 ∈ 𝐷 𝑟 = ( lastS ‘ 𝑑 ) )
75 fveq2 ⊢ ( 𝑡 = 𝑑 → ( lastS ‘ 𝑡 ) = ( lastS ‘ 𝑑 ) )
76 fvex ⊢ ( lastS ‘ 𝑑 ) ∈ V
77 75 5 76 fvmpt ⊢ ( 𝑑 ∈ 𝐷 → ( 𝐹 ‘ 𝑑 ) = ( lastS ‘ 𝑑 ) )
78 77 eqeq2d ⊢ ( 𝑑 ∈ 𝐷 → ( 𝑟 = ( 𝐹 ‘ 𝑑 ) ↔ 𝑟 = ( lastS ‘ 𝑑 ) ) )
79 78 rexbiia ⊢ ( ∃ 𝑑 ∈ 𝐷 𝑟 = ( 𝐹 ‘ 𝑑 ) ↔ ∃ 𝑑 ∈ 𝐷 𝑟 = ( lastS ‘ 𝑑 ) )
80 74 79 sylibr ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑟 ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , 𝑟 } ∈ 𝐸 ) ) → ∃ 𝑑 ∈ 𝐷 𝑟 = ( 𝐹 ‘ 𝑑 ) )
81 12 80 sylan2b ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑟 ∈ 𝑅 ) → ∃ 𝑑 ∈ 𝐷 𝑟 = ( 𝐹 ‘ 𝑑 ) )
82 81 ralrimiva ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∀ 𝑟 ∈ 𝑅 ∃ 𝑑 ∈ 𝐷 𝑟 = ( 𝐹 ‘ 𝑑 ) )
83 dffo3 ⊢ ( 𝐹 : 𝐷 –onto→ 𝑅 ↔ ( 𝐹 : 𝐷 ⟶ 𝑅 ∧ ∀ 𝑟 ∈ 𝑅 ∃ 𝑑 ∈ 𝐷 𝑟 = ( 𝐹 ‘ 𝑑 ) ) )
84 9 82 83 sylanbrc ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐹 : 𝐷 –onto→ 𝑅 )