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	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
	clwlkclwwlkf.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) − 1 ) ) )
Assertion	clwlkclwwlkf1o	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –1-1-onto→ ( ClWWalks ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlkf.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
2		clwlkclwwlkf.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2nd ‘ 𝑐 ) ) − 1 ) ) )
3	1 2	clwlkclwwlkf1	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –1-1→ ( ClWWalks ‘ 𝐺 ) )
4	1 2	clwlkclwwlkfo	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –onto→ ( ClWWalks ‘ 𝐺 ) )
5		df-f1o	⊢ ( 𝐹 : 𝐶 –1-1-onto→ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝐹 : 𝐶 –1-1→ ( ClWWalks ‘ 𝐺 ) ∧ 𝐹 : 𝐶 –onto→ ( ClWWalks ‘ 𝐺 ) ) )
6	3 4 5	sylanbrc	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –1-1-onto→ ( ClWWalks ‘ 𝐺 ) )