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

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 ( 𝑁 ∈ ℕ → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ≈ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V
2 1 rabex ⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ∈ V
3 ovex ⊢ ( 𝑁 ClWWalksN 𝐺 ) ∈ V
4 eqid ⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
5 eqid ⊢ ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) )
6 4 5 clwwlkf1o ⊢ ( 𝑁 ∈ ℕ → ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) ) : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )
7 f1oen2g ⊢ ( ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ∈ V ∧ ( 𝑁 ClWWalksN 𝐺 ) ∈ V ∧ ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) ) : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ≈ ( 𝑁 ClWWalksN 𝐺 ) )
8 2 3 6 7 mp3an12i ⊢ ( 𝑁 ∈ ℕ → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ≈ ( 𝑁 ClWWalksN 𝐺 ) )