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 ∈ n ClWWalksN G | 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 → n ClWWalksN g = n ClWWalksN G
4 3 rabeqdv ⊢ g = G → w ∈ n ClWWalksN g | w ⁡ 0 = v = w ∈ n ClWWalksN G | w ⁡ 0 = v
5 1 2 4 mpoeq123dv ⊢ g = G → v ∈ Vtx ⁡ g , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN g | w ⁡ 0 = v = v ∈ Vtx ⁡ G , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN G | w ⁡ 0 = v
6 df-clwwlknon ⊢ ClWWalksNOn = g ∈ V ⟼ v ∈ Vtx ⁡ g , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN g | w ⁡ 0 = v
7 fvex ⊢ Vtx ⁡ G ∈ V
8 nn0ex ⊢ ℕ 0 ∈ V
9 7 8 mpoex ⊢ v ∈ Vtx ⁡ G , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN G | w ⁡ 0 = v ∈ V
10 5 6 9 fvmpt ⊢ G ∈ V → ClWWalksNOn ⁡ G = v ∈ Vtx ⁡ G , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN G | 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 ∈ n ClWWalksN G | w ⁡ 0 = v = ∅
15 13 14 syl ⊢ ¬ G ∈ V → v ∈ Vtx ⁡ G , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN G | w ⁡ 0 = v = ∅
16 11 15 eqtr4d ⊢ ¬ G ∈ V → ClWWalksNOn ⁡ G = v ∈ Vtx ⁡ G , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN G | w ⁡ 0 = v
17 10 16 pm2.61i ⊢ ClWWalksNOn ⁡ G = v ∈ Vtx ⁡ G , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN G | w ⁡ 0 = v