Theorem clwwlkn

Description: The set of closed walks of a fixed length N as words over the set of vertices in a graph G . (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 22-Mar-2022)

	Ref	Expression
Assertion	clwwlkn	⊢ ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 }

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑔 = 𝐺 → ( ClWWalks ‘ 𝑔 ) = ( ClWWalks ‘ 𝐺 ) )
2	1	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ClWWalks ‘ 𝑔 ) = ( ClWWalks ‘ 𝐺 ) )
3		eqeq2	⊢ ( 𝑛 = 𝑁 → ( ( ♯ ‘ 𝑤 ) = 𝑛 ↔ ( ♯ ‘ 𝑤 ) = 𝑁 ) )
4	3	adantr	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = 𝑛 ↔ ( ♯ ‘ 𝑤 ) = 𝑁 ) )
5	2 4	rabeqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } )
6		df-clwwlkn	⊢ ClWWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )
7		fvex	⊢ ( ClWWalks ‘ 𝐺 ) ∈ V
8	7	rabex	⊢ { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ V
9	5 6 8	ovmpoa	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } )
10	6	mpondm0	⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
11		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
12	11	clwwlkbp	⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑤 ≠ ∅ ) )
13	12	simp2d	⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
14		lencl	⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
15	13 14	syl	⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
16		eleq1	⊢ ( ( ♯ ‘ 𝑤 ) = 𝑁 → ( ( ♯ ‘ 𝑤 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
17	15 16	syl5ibcom	⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = 𝑁 → 𝑁 ∈ ℕ0 ) )
18	17	con3rr3	⊢ ( ¬ 𝑁 ∈ ℕ0 → ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) )
19	18	ralrimiv	⊢ ( ¬ 𝑁 ∈ ℕ0 → ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 )
20		ral0	⊢ ∀ 𝑤 ∈ ∅ ¬ ( ♯ ‘ 𝑤 ) = 𝑁
21		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( ClWWalks ‘ 𝐺 ) = ∅ )
22	21	raleqdv	⊢ ( ¬ 𝐺 ∈ V → ( ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ↔ ∀ 𝑤 ∈ ∅ ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) )
23	20 22	mpbiri	⊢ ( ¬ 𝐺 ∈ V → ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 )
24	19 23	jaoi	⊢ ( ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝐺 ∈ V ) → ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 )
25		ianor	⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ↔ ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝐺 ∈ V ) )
26		rabeq0	⊢ ( { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ∅ ↔ ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 )
27	24 25 26	3imtr4i	⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ∅ )
28	10 27	eqtr4d	⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } )
29	9 28	pm2.61i	⊢ ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 }