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	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( ClWalks ‘ 𝐺 ) ∈ V
2	1	rabex	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∈ V
3		ovex	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ V
4		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5		eqid	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
6		eqid	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
7	4 5 6	clwwlknonclwlknonf1o	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
8		f1oen2g	⊢ ( ( { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∈ V ∧ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ V ∧ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
9	2 3 7 8	mp3an12i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ≈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )