# 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 ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
wwlksnextbij0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
wwlksnextbij0.d ${⊢}{D}=\left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|={N}+2\wedge {w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}$
wwlksnextbij0.r ${⊢}{R}=\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}$
wwlksnextbij0.f ${⊢}{F}=\left({t}\in {D}⟼\mathrm{lastS}\left({t}\right)\right)$
Assertion wwlksnextsurj ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to {F}:{D}\underset{onto}{⟶}{R}$

### Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 wwlksnextbij0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 wwlksnextbij0.d ${⊢}{D}=\left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|={N}+2\wedge {w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}$
4 wwlksnextbij0.r ${⊢}{R}=\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}$
5 wwlksnextbij0.f ${⊢}{F}=\left({t}\in {D}⟼\mathrm{lastS}\left({t}\right)\right)$
6 1 wwlknbp ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({G}\in \mathrm{V}\wedge {N}\in {ℕ}_{0}\wedge {W}\in \mathrm{Word}{V}\right)$
7 simp2 ${⊢}\left({G}\in \mathrm{V}\wedge {N}\in {ℕ}_{0}\wedge {W}\in \mathrm{Word}{V}\right)\to {N}\in {ℕ}_{0}$
8 1 2 3 4 5 wwlksnextfun ${⊢}{N}\in {ℕ}_{0}\to {F}:{D}⟶{R}$
9 6 7 8 3syl ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to {F}:{D}⟶{R}$
10 preq2 ${⊢}{n}={r}\to \left\{\mathrm{lastS}\left({W}\right),{n}\right\}=\left\{\mathrm{lastS}\left({W}\right),{r}\right\}$
11 10 eleq1d ${⊢}{n}={r}\to \left(\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}↔\left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)$
12 11 4 elrab2 ${⊢}{r}\in {R}↔\left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)$
13 1 2 wwlksnext ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge {r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\to {W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)$
14 13 3expb ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to {W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)$
15 s1cl ${⊢}{r}\in {V}\to ⟨“{r}”⟩\in \mathrm{Word}{V}$
16 pfxccat1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge ⟨“{r}”⟩\in \mathrm{Word}{V}\right)\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|={W}$
17 15 16 sylan2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {r}\in {V}\right)\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|={W}$
18 17 ex ${⊢}{W}\in \mathrm{Word}{V}\to \left({r}\in {V}\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|={W}\right)$
19 18 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}+1\right)\to \left({r}\in {V}\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|={W}\right)$
20 oveq2 ${⊢}{N}+1=\left|{W}\right|\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)=\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|$
21 20 eqcoms ${⊢}\left|{W}\right|={N}+1\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)=\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|$
22 21 eqeq1d ${⊢}\left|{W}\right|={N}+1\to \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}↔\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|={W}\right)$
23 22 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}+1\right)\to \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}↔\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left|{W}\right|={W}\right)$
24 19 23 sylibrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}+1\right)\to \left({r}\in {V}\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\right)$
25 24 3adant3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}+1\wedge \forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\right)\to \left({r}\in {V}\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\right)$
26 1 2 wwlknp ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}+1\wedge \forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\right)$
27 25 26 syl11 ${⊢}{r}\in {V}\to \left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\right)$
28 27 adantr ${⊢}\left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\to \left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\right)$
29 28 impcom ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}$
30 lswccats1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {r}\in {V}\right)\to \mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)={r}$
31 30 eqcomd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {r}\in {V}\right)\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)$
32 31 ex ${⊢}{W}\in \mathrm{Word}{V}\to \left({r}\in {V}\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)$
33 32 3ad2ant3 ${⊢}\left({G}\in \mathrm{V}\wedge {N}\in {ℕ}_{0}\wedge {W}\in \mathrm{Word}{V}\right)\to \left({r}\in {V}\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)$
34 6 33 syl ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({r}\in {V}\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)$
35 34 imp ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge {r}\in {V}\right)\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)$
36 35 preq2d ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge {r}\in {V}\right)\to \left\{\mathrm{lastS}\left({W}\right),{r}\right\}=\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}$
37 36 eleq1d ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge {r}\in {V}\right)\to \left(\left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}↔\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)$
38 37 biimpd ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge {r}\in {V}\right)\to \left(\left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\to \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)$
39 38 impr ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}$
40 14 29 39 jca32 ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \left({W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)$
41 33 6 syl11 ${⊢}{r}\in {V}\to \left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)$
42 41 adantr ${⊢}\left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\to \left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)$
43 42 impcom ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)$
44 ovexd ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to {W}\mathrm{++}⟨“{r}”⟩\in \mathrm{V}$
45 eleq1 ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)↔{W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\right)$
46 oveq1 ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to {d}\mathrm{prefix}\left({N}+1\right)=\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)$
47 46 eqeq1d ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left({d}\mathrm{prefix}\left({N}+1\right)={W}↔\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\right)$
48 fveq2 ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \mathrm{lastS}\left({d}\right)=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)$
49 48 preq2d ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}=\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}$
50 49 eleq1d ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left(\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}↔\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)$
51 47 50 anbi12d ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left(\left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)↔\left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)$
52 45 51 anbi12d ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)↔\left({W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)\right)$
53 48 eqeq2d ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left({r}=\mathrm{lastS}\left({d}\right)↔{r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)$
54 52 53 anbi12d ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left(\left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)↔\left(\left({W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)\right)$
55 54 bicomd ${⊢}{d}={W}\mathrm{++}⟨“{r}”⟩\to \left(\left(\left({W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)↔\left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)\right)$
56 55 adantl ${⊢}\left(\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\wedge {d}={W}\mathrm{++}⟨“{r}”⟩\right)\to \left(\left(\left({W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)↔\left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)\right)$
57 56 biimpd ${⊢}\left(\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\wedge {d}={W}\mathrm{++}⟨“{r}”⟩\right)\to \left(\left(\left({W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)\to \left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)\right)$
58 44 57 spcimedv ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \left(\left(\left({W}\mathrm{++}⟨“{r}”⟩\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left(\left({W}\mathrm{++}⟨“{r}”⟩\right)\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({W}\mathrm{++}⟨“{r}”⟩\right)\right)\to \exists {d}\phantom{\rule{.4em}{0ex}}\left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)\right)$
59 40 43 58 mp2and ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \exists {d}\phantom{\rule{.4em}{0ex}}\left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)$
60 oveq1 ${⊢}{w}={d}\to {w}\mathrm{prefix}\left({N}+1\right)={d}\mathrm{prefix}\left({N}+1\right)$
61 60 eqeq1d ${⊢}{w}={d}\to \left({w}\mathrm{prefix}\left({N}+1\right)={W}↔{d}\mathrm{prefix}\left({N}+1\right)={W}\right)$
62 fveq2 ${⊢}{w}={d}\to \mathrm{lastS}\left({w}\right)=\mathrm{lastS}\left({d}\right)$
63 62 preq2d ${⊢}{w}={d}\to \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}=\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}$
64 63 eleq1d ${⊢}{w}={d}\to \left(\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}↔\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)$
65 61 64 anbi12d ${⊢}{w}={d}\to \left(\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)↔\left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)$
66 65 elrab ${⊢}{d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}↔\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)$
67 66 anbi1i ${⊢}\left({d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}\wedge {r}=\mathrm{lastS}\left({d}\right)\right)↔\left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)$
68 67 exbii ${⊢}\exists {d}\phantom{\rule{.4em}{0ex}}\left({d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}\wedge {r}=\mathrm{lastS}\left({d}\right)\right)↔\exists {d}\phantom{\rule{.4em}{0ex}}\left(\left({d}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)\wedge \left({d}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({d}\right)\right\}\in {E}\right)\right)\wedge {r}=\mathrm{lastS}\left({d}\right)\right)$
69 59 68 sylibr ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \exists {d}\phantom{\rule{.4em}{0ex}}\left({d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}\wedge {r}=\mathrm{lastS}\left({d}\right)\right)$
70 df-rex ${⊢}\exists {d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}\phantom{\rule{.4em}{0ex}}{r}=\mathrm{lastS}\left({d}\right)↔\exists {d}\phantom{\rule{.4em}{0ex}}\left({d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}\wedge {r}=\mathrm{lastS}\left({d}\right)\right)$
71 69 70 sylibr ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \exists {d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}\phantom{\rule{.4em}{0ex}}{r}=\mathrm{lastS}\left({d}\right)$
72 1 2 3 wwlksnextwrd ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to {D}=\left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}$
73 72 adantr ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to {D}=\left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}$
74 73 rexeqdv ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \left(\exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}=\mathrm{lastS}\left({d}\right)↔\exists {d}\in \left\{{w}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({w}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)\right\}\phantom{\rule{.4em}{0ex}}{r}=\mathrm{lastS}\left({d}\right)\right)$
75 71 74 mpbird ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}=\mathrm{lastS}\left({d}\right)$
76 fveq2 ${⊢}{t}={d}\to \mathrm{lastS}\left({t}\right)=\mathrm{lastS}\left({d}\right)$
77 fvex ${⊢}\mathrm{lastS}\left({d}\right)\in \mathrm{V}$
78 76 5 77 fvmpt ${⊢}{d}\in {D}\to {F}\left({d}\right)=\mathrm{lastS}\left({d}\right)$
79 78 eqeq2d ${⊢}{d}\in {D}\to \left({r}={F}\left({d}\right)↔{r}=\mathrm{lastS}\left({d}\right)\right)$
80 79 rexbiia ${⊢}\exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}={F}\left({d}\right)↔\exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}=\mathrm{lastS}\left({d}\right)$
81 75 80 sylibr ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \left({r}\in {V}\wedge \left\{\mathrm{lastS}\left({W}\right),{r}\right\}\in {E}\right)\right)\to \exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}={F}\left({d}\right)$
82 12 81 sylan2b ${⊢}\left({W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge {r}\in {R}\right)\to \exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}={F}\left({d}\right)$
83 82 ralrimiva ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}={F}\left({d}\right)$
84 dffo3 ${⊢}{F}:{D}\underset{onto}{⟶}{R}↔\left({F}:{D}⟶{R}\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {d}\in {D}\phantom{\rule{.4em}{0ex}}{r}={F}\left({d}\right)\right)$
85 9 83 84 sylanbrc ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to {F}:{D}\underset{onto}{⟶}{R}$