Theorem clwlkclwwlkf1o

Description: F is a bijection between the nonempty closed walks and the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 29-Oct-2022)

	Ref	Expression
Hypotheses	clwlkclwwlkf.c	$$⊢C=\left\{w\in \mathrm{ClWalks}\left(G\right)|1\le \left|1^{st}\left(w\right)\right|\right\}$$
	clwlkclwwlkf.f	$$⊢F=\left(c\in C⟼2^{nd}\left(c\right)\mathrm{prefix}\left(\left|2^{nd}\left(c\right)\right|-1\right)\right)$$
Assertion	clwlkclwwlkf1o	$$⊢G\in \mathrm{USHGraph}\to F:C\underset{1-1\; onto}{⟶}\mathrm{ClWWalks}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlkf.c	$$⊢C=\left\{w\in \mathrm{ClWalks}\left(G\right)|1\le \left|1^{st}\left(w\right)\right|\right\}$$
2		clwlkclwwlkf.f	$$⊢F=\left(c\in C⟼2^{nd}\left(c\right)\mathrm{prefix}\left(\left|2^{nd}\left(c\right)\right|-1\right)\right)$$
3	1 2	clwlkclwwlkf1	$$⊢G\in \mathrm{USHGraph}\to F:C\underset{1-1}{⟶}\mathrm{ClWWalks}\left(G\right)$$
4	1 2	clwlkclwwlkfo	$$⊢G\in \mathrm{USHGraph}\to F:C\underset{onto}{⟶}\mathrm{ClWWalks}\left(G\right)$$
5		df-f1o	$$⊢F:C\underset{1-1\; onto}{⟶}\mathrm{ClWWalks}\left(G\right)\leftrightarrow \left(F:C\underset{1-1}{⟶}\mathrm{ClWWalks}\left(G\right)\wedge F:C\underset{onto}{⟶}\mathrm{ClWWalks}\left(G\right)\right)$$
6	3 4 5	sylanbrc	$$⊢G\in \mathrm{USHGraph}\to F:C\underset{1-1\; onto}{⟶}\mathrm{ClWWalks}\left(G\right)$$