Metamath Proof Explorer

Theorem clwwlknonmpo

Description: ( ClWWalksNOnG ) is an operator mapping a vertex v and a nonnegative integer n to the set of closed walks on v of length n as words over the set of vertices in a graph G . (Contributed by AV, 25-Feb-2022) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Assertion clwwlknonmpo ⊢ClWWalksNOn⁡G=v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v

Proof

Step Hyp Ref Expression
1 fveq2 ⊢g=G→Vtx⁡g=Vtx⁡G
2 eqidd ⊢g=G→ℕ0=ℕ0
3 oveq2 ⊢g=G→nClWWalksNg=nClWWalksNG
4 3 rabeqdv ⊢g=G→w∈nClWWalksNg|w⁡0=v=w∈nClWWalksNG|w⁡0=v
5 1 2 4 mpoeq123dv ⊢g=G→v∈Vtx⁡g,n∈ℕ0⟼w∈nClWWalksNg|w⁡0=v=v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v
6 df-clwwlknon ⊢ClWWalksNOn=g∈V⟼v∈Vtx⁡g,n∈ℕ0⟼w∈nClWWalksNg|w⁡0=v
7 fvex ⊢Vtx⁡G∈V
8 nn0ex ⊢ℕ0∈V
9 7 8 mpoex ⊢v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v∈V
10 5 6 9 fvmpt ⊢G∈V→ClWWalksNOn⁡G=v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v
11 fvprc ⊢¬G∈V→ClWWalksNOn⁡G=∅
12 fvprc ⊢¬G∈V→Vtx⁡G=∅
13 12 orcd ⊢¬G∈V→Vtx⁡G=∅∨ℕ0=∅
14 0mpo0 ⊢Vtx⁡G=∅∨ℕ0=∅→v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v=∅
15 13 14 syl ⊢¬G∈V→v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v=∅
16 11 15 eqtr4d ⊢¬G∈V→ClWWalksNOn⁡G=v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v
17 10 16 pm2.61i ⊢ClWWalksNOn⁡G=v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v