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