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 𝐶 = { 𝑤 ∈ ( 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 ‘ 𝐺 ) )