Metamath Proof Explorer

Theorem clwlkssizeeq

Description: The size of the set of closed walks as words of length N corresponds to the size of the set of closed walks of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 4-May-2021) (Revised by AV, 26-May-2022) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Assertion clwlkssizeeq ⊢ G ∈ USHGraph ∧ N ∈ ℕ → N ClWWalksN G = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N

Proof

Step Hyp Ref Expression
1 fvex ⊢ ClWalks ⁡ G ∈ V
2 1 rabex ⊢ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∈ V
3 2 a1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ → w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∈ V
4 eqid ⊢ 1 st ⁡ c = 1 st ⁡ c
5 eqid ⊢ 2 nd ⁡ c = 2 nd ⁡ c
6 eqid ⊢ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N
7 eqid ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ⟼ 2 nd ⁡ c prefix 1 st ⁡ c = c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ⟼ 2 nd ⁡ c prefix 1 st ⁡ c
8 4 5 6 7 clwlknf1oclwwlkn ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ⟼ 2 nd ⁡ c prefix 1 st ⁡ c : w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ⟶ 1-1 onto N ClWWalksN G
9 3 8 hasheqf1od ⊢ G ∈ USHGraph ∧ N ∈ ℕ → w ∈ ClWalks ⁡ G | 1 st ⁡ w = N = N ClWWalksN G
10 9 eqcomd ⊢ G ∈ USHGraph ∧ N ∈ ℕ → N ClWWalksN G = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N