Description: The set of walks as words and the set of (ordinary) walks are equinumerous in a simple pseudograph. (Contributed by AV, 6-May-2021) (Revised by AV, 5-Aug-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | wlkswwlksen | ⊢ ( 𝐺 ∈ USPGraph → ( Walks ‘ 𝐺 ) ≈ ( WWalks ‘ 𝐺 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑤 ) ) = ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑤 ) ) | |
2 | 1 | wlkswwlksf1o | ⊢ ( 𝐺 ∈ USPGraph → ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑤 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) ) |
3 | fvex | ⊢ ( Walks ‘ 𝐺 ) ∈ V | |
4 | 3 | f1oen | ⊢ ( ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑤 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) → ( Walks ‘ 𝐺 ) ≈ ( WWalks ‘ 𝐺 ) ) |
5 | 2 4 | syl | ⊢ ( 𝐺 ∈ USPGraph → ( Walks ‘ 𝐺 ) ≈ ( WWalks ‘ 𝐺 ) ) |