Metamath Proof Explorer

Theorem clwwlknonclwlknonen

Description: The sets of the two representations of closed walks of a fixed positive length on a fixed vertex are equinumerous. (Contributed by AV, 27-May-2022) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Assertion clwwlknonclwlknonen ⊢G∈USHGraph∧X∈Vtx⁡G∧N∈ℕ→w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X≈XClWWalksNOn⁡GN

Proof

Step Hyp Ref Expression
1 fvex ⊢ClWalks⁡G∈V
2 1 rabex ⊢w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X∈V
3 ovex ⊢XClWWalksNOn⁡GN∈V
4 eqid ⊢Vtx⁡G=Vtx⁡G
5 eqid ⊢w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X=w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X
6 eqid ⊢c∈w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X⟼2nd⁡cprefix1st⁡c=c∈w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X⟼2nd⁡cprefix1st⁡c
7 4 5 6 clwwlknonclwlknonf1o ⊢G∈USHGraph∧X∈Vtx⁡G∧N∈ℕ→c∈w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X⟼2nd⁡cprefix1st⁡c:w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X⟶1-1 ontoXClWWalksNOn⁡GN
8 f1oen2g ⊢w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X∈V∧XClWWalksNOn⁡GN∈V∧c∈w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X⟼2nd⁡cprefix1st⁡c:w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X⟶1-1 ontoXClWWalksNOn⁡GN→w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X≈XClWWalksNOn⁡GN
9 2 3 7 8 mp3an12i ⊢G∈USHGraph∧X∈Vtx⁡G∧N∈ℕ→w∈ClWalks⁡G|1st⁡w=N∧2nd⁡w⁡0=X≈XClWWalksNOn⁡GN