# Metamath Proof Explorer

## Theorem wwlksnextbij

Description: There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
wwlksnextbij.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion wwlksnextbij ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}$

### Proof

Step Hyp Ref Expression
1 wwlksnextbij.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 wwlksnextbij.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 ovexd ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({N}+1\right)\mathrm{WWalksN}{G}\in \mathrm{V}$
4 rabexg ${⊢}\left({N}+1\right)\mathrm{WWalksN}{G}\in \mathrm{V}\to \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}\in \mathrm{V}$
5 mptexg ${⊢}\left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}\in \mathrm{V}\to \left({x}\in \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right)\in \mathrm{V}$
6 3 4 5 3syl ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({x}\in \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right)\in \mathrm{V}$
7 eqid ${⊢}\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\}=\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\}$
8 preq2 ${⊢}{n}={p}\to \left\{\mathrm{lastS}\left({W}\right),{n}\right\}=\left\{\mathrm{lastS}\left({W}\right),{p}\right\}$
9 8 eleq1d ${⊢}{n}={p}\to \left(\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}↔\left\{\mathrm{lastS}\left({W}\right),{p}\right\}\in {E}\right)$
10 9 cbvrabv ${⊢}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}=\left\{{p}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{p}\right\}\in {E}\right\}$
11 fveqeq2 ${⊢}{t}={w}\to \left(\left|{t}\right|={N}+2↔\left|{w}\right|={N}+2\right)$
12 oveq1 ${⊢}{t}={w}\to {t}\mathrm{prefix}\left({N}+1\right)={w}\mathrm{prefix}\left({N}+1\right)$
13 12 eqeq1d ${⊢}{t}={w}\to \left({t}\mathrm{prefix}\left({N}+1\right)={W}↔{w}\mathrm{prefix}\left({N}+1\right)={W}\right)$
14 fveq2 ${⊢}{t}={w}\to \mathrm{lastS}\left({t}\right)=\mathrm{lastS}\left({w}\right)$
15 14 preq2d ${⊢}{t}={w}\to \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}=\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}$
16 15 eleq1d ${⊢}{t}={w}\to \left(\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}↔\left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({w}\right)\right\}\in {E}\right)$
17 11 13 16 3anbi123d ${⊢}{t}={w}\to \left(\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)↔\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)$
18 17 cbvrabv ${⊢}\left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}=\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\}$
19 18 mpteq1i ${⊢}\left({x}\in \left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right)=\left({x}\in \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\}⟼\mathrm{lastS}\left({x}\right)\right)$
20 1 2 7 10 19 wwlksnextbij0 ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({x}\in \left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right):\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}$
21 eqid ${⊢}\left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}=\left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}$
22 1 2 21 wwlksnextwrd ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}=\left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}$
23 22 eqcomd ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}=\left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}$
24 23 mpteq1d ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({x}\in \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right)=\left({x}\in \left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right)$
25 1 2 7 wwlksnextwrd ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \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\}=\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\}$
26 25 eqcomd ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \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\{{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\}$
27 eqidd ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}=\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}$
28 24 26 27 f1oeq123d ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left(\left({x}\in \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right):\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}↔\left({x}\in \left\{{t}\in \mathrm{Word}{V}|\left(\left|{t}\right|={N}+2\wedge {t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right):\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}\right)$
29 20 28 mpbird ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({x}\in \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right):\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}$
30 f1oeq1 ${⊢}{f}=\left({x}\in \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right)\to \left({f}:\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}↔\left({x}\in \left\{{t}\in \left(\left({N}+1\right)\mathrm{WWalksN}{G}\right)|\left({t}\mathrm{prefix}\left({N}+1\right)={W}\wedge \left\{\mathrm{lastS}\left({W}\right),\mathrm{lastS}\left({t}\right)\right\}\in {E}\right)\right\}⟼\mathrm{lastS}\left({x}\right)\right):\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}\right)$
31 6 29 30 spcedv ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\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\}\underset{1-1 onto}{⟶}\left\{{n}\in {V}|\left\{\mathrm{lastS}\left({W}\right),{n}\right\}\in {E}\right\}$