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 ⊢ N ClWWalksN G = w ∈ ClWWalks ⁡ G | w = N

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ g = G → ClWWalks ⁡ g = ClWWalks ⁡ G
2 1 adantl ⊢ n = N ∧ g = G → ClWWalks ⁡ g = ClWWalks ⁡ G
3 eqeq2 ⊢ n = N → w = n ↔ w = N
4 3 adantr ⊢ n = N ∧ g = G → w = n ↔ w = N
5 2 4 rabeqbidv ⊢ n = N ∧ g = G → w ∈ ClWWalks ⁡ g | w = n = w ∈ ClWWalks ⁡ G | w = N
6 df-clwwlkn ⊢ ClWWalksN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ ClWWalks ⁡ g | w = n
7 fvex ⊢ ClWWalks ⁡ G ∈ V
8 7 rabex ⊢ w ∈ ClWWalks ⁡ G | w = N ∈ V
9 5 6 8 ovmpoa ⊢ N ∈ ℕ 0 ∧ G ∈ V → N ClWWalksN G = w ∈ ClWWalks ⁡ G | w = N
10 6 mpondm0 ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N ClWWalksN G = ∅
11 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
12 11 clwwlkbp ⊢ w ∈ ClWWalks ⁡ G → G ∈ V ∧ w ∈ Word Vtx ⁡ G ∧ w ≠ ∅
13 12 simp2d ⊢ w ∈ ClWWalks ⁡ G → w ∈ Word Vtx ⁡ G
14 lencl ⊢ w ∈ Word Vtx ⁡ G → w ∈ ℕ 0
15 13 14 syl ⊢ w ∈ ClWWalks ⁡ G → w ∈ ℕ 0
16 eleq1 ⊢ w = N → w ∈ ℕ 0 ↔ N ∈ ℕ 0
17 15 16 syl5ibcom ⊢ w ∈ ClWWalks ⁡ G → w = N → N ∈ ℕ 0
18 17 con3rr3 ⊢ ¬ N ∈ ℕ 0 → w ∈ ClWWalks ⁡ G → ¬ w = N
19 18 ralrimiv ⊢ ¬ N ∈ ℕ 0 → ∀ w ∈ ClWWalks ⁡ G ¬ w = N
20 ral0 ⊢ ∀ w ∈ ∅ ¬ w = N
21 fvprc ⊢ ¬ G ∈ V → ClWWalks ⁡ G = ∅
22 21 raleqdv ⊢ ¬ G ∈ V → ∀ w ∈ ClWWalks ⁡ G ¬ w = N ↔ ∀ w ∈ ∅ ¬ w = N
23 20 22 mpbiri ⊢ ¬ G ∈ V → ∀ w ∈ ClWWalks ⁡ G ¬ w = N
24 19 23 jaoi ⊢ ¬ N ∈ ℕ 0 ∨ ¬ G ∈ V → ∀ w ∈ ClWWalks ⁡ G ¬ w = N
25 ianor ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V ↔ ¬ N ∈ ℕ 0 ∨ ¬ G ∈ V
26 rabeq0 ⊢ w ∈ ClWWalks ⁡ G | w = N = ∅ ↔ ∀ w ∈ ClWWalks ⁡ G ¬ w = N
27 24 25 26 3imtr4i ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → w ∈ ClWWalks ⁡ G | w = N = ∅
28 10 27 eqtr4d ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N ClWWalksN G = w ∈ ClWWalks ⁡ G | w = N
29 9 28 pm2.61i ⊢ N ClWWalksN G = w ∈ ClWWalks ⁡ G | w = N