Metamath Proof Explorer

Theorem clwwlk0on0

Description: There is no word over the set of vertices representing a closed walk on vertex X of length 0 in a graph G . (Contributed by AV, 17-Feb-2022) (Revised by AV, 25-Feb-2022)

Ref Expression
Assertion clwwlk0on0 ⊢ X ClWWalksNOn ⁡ G 0 = ∅

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ v = X → w ⁡ 0 = v ↔ w ⁡ 0 = X
2 1 rabbidv ⊢ v = X → w ∈ n ClWWalksN G | w ⁡ 0 = v = w ∈ n ClWWalksN G | w ⁡ 0 = X
3 oveq1 ⊢ n = 0 → n ClWWalksN G = 0 ClWWalksN G
4 clwwlkn0 ⊢ 0 ClWWalksN G = ∅
5 3 4 eqtrdi ⊢ n = 0 → n ClWWalksN G = ∅
6 5 rabeqdv ⊢ n = 0 → w ∈ n ClWWalksN G | w ⁡ 0 = X = w ∈ ∅ | w ⁡ 0 = X
7 clwwlknonmpo ⊢ ClWWalksNOn ⁡ G = v ∈ Vtx ⁡ G , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN G | w ⁡ 0 = v
8 0ex ⊢ ∅ ∈ V
9 8 rabex ⊢ w ∈ ∅ | w ⁡ 0 = X ∈ V
10 2 6 7 9 ovmpo ⊢ X ∈ Vtx ⁡ G ∧ 0 ∈ ℕ 0 → X ClWWalksNOn ⁡ G 0 = w ∈ ∅ | w ⁡ 0 = X
11 rab0 ⊢ w ∈ ∅ | w ⁡ 0 = X = ∅
12 10 11 eqtrdi ⊢ X ∈ Vtx ⁡ G ∧ 0 ∈ ℕ 0 → X ClWWalksNOn ⁡ G 0 = ∅
13 7 mpondm0 ⊢ ¬ X ∈ Vtx ⁡ G ∧ 0 ∈ ℕ 0 → X ClWWalksNOn ⁡ G 0 = ∅
14 12 13 pm2.61i ⊢ X ClWWalksNOn ⁡ G 0 = ∅