Metamath Proof Explorer


Theorem wlkswwlksen

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

Proof

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