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	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( ClWalks ‘ 𝐺 ) ∈ V
2	1	rabex	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ∈ V
3	2	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ∈ V )
4		eqid	⊢ ( 1^st ‘ 𝑐 ) = ( 1^st ‘ 𝑐 )
5		eqid	⊢ ( 2^nd ‘ 𝑐 ) = ( 2^nd ‘ 𝑐 )
6		eqid	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 }
7		eqid	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
8	4 5 6 7	clwlknf1oclwwlkn	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )
9	3 8	hasheqf1od	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) )
10	9	eqcomd	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ) )

Metamath Proof Explorer

Theorem clwlkssizeeq

Proof