This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ G ∈ USHGraph → Walks ⁡ G ≈ WWalks ⁡ G

Proof

Step Hyp Ref Expression
1 eqid ⊢ w ∈ Walks ⁡ G ⟼ 2 nd ⁡ w = w ∈ Walks ⁡ G ⟼ 2 nd ⁡ w
2 1 wlkswwlksf1o ⊢ G ∈ USHGraph → w ∈ Walks ⁡ G ⟼ 2 nd ⁡ w : Walks ⁡ G ⟶ 1-1 onto WWalks ⁡ G
3 fvex ⊢ Walks ⁡ G ∈ V
4 3 f1oen ⊢ w ∈ Walks ⁡ G ⟼ 2 nd ⁡ w : Walks ⁡ G ⟶ 1-1 onto WWalks ⁡ G → Walks ⁡ G ≈ WWalks ⁡ G
5 2 4 syl ⊢ G ∈ USHGraph → Walks ⁡ G ≈ WWalks ⁡ G