Metamath Proof Explorer


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 ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 }