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

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