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 | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ≈ X ClWWalksNOn ⁡ G N

Proof

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