Theorem wlkswwlksen

Description: The set of walks as words and the set of (ordinary) walks are equinumerous in a simple pseudograph. (Contributed by AV, 6-May-2021) (Revised by AV, 5-Aug-2022)

	Ref	Expression
Assertion	wlkswwlksen	$$⊢G\in \mathrm{USHGraph}\to \mathrm{Walks}\left(G\right)\approx \mathrm{WWalks}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(w\in \mathrm{Walks}\left(G\right)⟼2^{nd}\left(w\right)\right)=\left(w\in \mathrm{Walks}\left(G\right)⟼2^{nd}\left(w\right)\right)$$
2	1	wlkswwlksf1o	$$⊢G\in \mathrm{USHGraph}\to \left(w\in \mathrm{Walks}\left(G\right)⟼2^{nd}\left(w\right)\right):\mathrm{Walks}\left(G\right)\underset{1-1\; onto}{⟶}\mathrm{WWalks}\left(G\right)$$
3		fvex	$$⊢\mathrm{Walks}\left(G\right)\in \mathrm{V}$$
4	3	f1oen	$$⊢\left(w\in \mathrm{Walks}\left(G\right)⟼2^{nd}\left(w\right)\right):\mathrm{Walks}\left(G\right)\underset{1-1\; onto}{⟶}\mathrm{WWalks}\left(G\right)\to \mathrm{Walks}\left(G\right)\approx \mathrm{WWalks}\left(G\right)$$
5	2 4	syl	$$⊢G\in \mathrm{USHGraph}\to \mathrm{Walks}\left(G\right)\approx \mathrm{WWalks}\left(G\right)$$