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 ‘ 𝐺 ) ) |
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 ‘ 𝐺 ) ) |