This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\}$
		clwlkclwwlkf.f	$⊢ F = (c \in C ⟼ 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1))$
	Assertion	clwlkclwwlkf1o	$⊢ G \in USHGraph \to F : C \underset{1-1 onto}{⟶} ClWWalks (G)$

Proof

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