Metamath Proof Explorer

Theorem clwwlken

Description: The set of closed walks of a fixed length represented by walks (as words) and the set of closed walks (as words) of the fixed length are equinumerous. (Contributed by AV, 5-Jun-2022) (Proof shortened by AV, 2-Nov-2022)

Ref Expression
Assertion clwwlken ⊢ N ∈ ℕ → w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ≈ N ClWWalksN G

Proof

Step Hyp Ref Expression
1 ovex ⊢ N WWalksN G ∈ V
2 1 rabex ⊢ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∈ V
3 ovex ⊢ N ClWWalksN G ∈ V
4 eqid ⊢ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0
5 eqid ⊢ c ∈ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ⟼ c prefix N = c ∈ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ⟼ c prefix N
6 4 5 clwwlkf1o ⊢ N ∈ ℕ → c ∈ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ⟼ c prefix N : w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ⟶ 1-1 onto N ClWWalksN G
7 f1oen2g ⊢ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∈ V ∧ N ClWWalksN G ∈ V ∧ c ∈ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ⟼ c prefix N : w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ⟶ 1-1 onto N ClWWalksN G → w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ≈ N ClWWalksN G
8 2 3 6 7 mp3an12i ⊢ N ∈ ℕ → w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ≈ N ClWWalksN G