Metamath Proof Explorer

Theorem numclwwlk3lem2lem

Description: Lemma for numclwwlk3lem2 : The set of closed vertices of a fixed length N on a fixed vertex V is the union of the set of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk3lem2.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
numclwwlk3lem2.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
Assertion numclwwlk3lem2lem ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X ClWWalksNOn ⁡ G N = X H N ∪ X C N

Proof

Step Hyp Ref Expression
1 numclwwlk3lem2.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
2 numclwwlk3lem2.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
3 2 numclwwlkovh0 ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X
4 1 2clwwlk ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
5 3 4 uneq12d ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N ∪ X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∪ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
6 unrab ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∪ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∨ w ⁡ N − 2 = X
7 exmidne ⊢ w ⁡ N − 2 = X ∨ w ⁡ N − 2 ≠ X
8 orcom ⊢ w ⁡ N − 2 ≠ X ∨ w ⁡ N − 2 = X ↔ w ⁡ N − 2 = X ∨ w ⁡ N − 2 ≠ X
9 7 8 mpbir ⊢ w ⁡ N − 2 ≠ X ∨ w ⁡ N − 2 = X
10 9 a1i ⊢ w ∈ X ClWWalksNOn ⁡ G N → w ⁡ N − 2 ≠ X ∨ w ⁡ N − 2 = X
11 10 rabeqc ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∨ w ⁡ N − 2 = X = X ClWWalksNOn ⁡ G N
12 6 11 eqtri ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∪ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X = X ClWWalksNOn ⁡ G N
13 5 12 eqtr2di ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X ClWWalksNOn ⁡ G N = X H N ∪ X C N