Metamath Proof Explorer

Theorem clwwlknclwwlkdif

Description: The set A of walks of length N starting with a fixed vertex V and ending not at this vertex is the difference between the set C of walks of length N starting with this vertex X and the set B of closed walks of length N anchored at this vertex X . (Contributed by Alexander van der Vekens, 30-Sep-2018) (Revised by AV, 7-May-2021) (Revised by AV, 16-Mar-2022)

Ref Expression
Hypotheses clwwlknclwwlkdif.a ⊢ A = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
clwwlknclwwlkdif.b ⊢ B = X N WWalksNOn G X
clwwlknclwwlkdif.c ⊢ C = w ∈ N WWalksN G | w ⁡ 0 = X
Assertion clwwlknclwwlkdif ⊢ A = C ∖ B

Proof

Step Hyp Ref Expression
1 clwwlknclwwlkdif.a ⊢ A = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
2 clwwlknclwwlkdif.b ⊢ B = X N WWalksNOn G X
3 clwwlknclwwlkdif.c ⊢ C = w ∈ N WWalksN G | w ⁡ 0 = X
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 iswwlksnon ⊢ X N WWalksNOn G X = w ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X
6 2 5 eqtri ⊢ B = w ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X
7 3 6 difeq12i ⊢ C ∖ B = w ∈ N WWalksN G | w ⁡ 0 = X ∖ w ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X
8 difrab ⊢ w ∈ N WWalksN G | w ⁡ 0 = X ∖ w ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X = w ∈ N WWalksN G | w ⁡ 0 = X ∧ ¬ w ⁡ 0 = X ∧ w ⁡ N = X
9 annotanannot ⊢ w ⁡ 0 = X ∧ ¬ w ⁡ 0 = X ∧ w ⁡ N = X ↔ w ⁡ 0 = X ∧ ¬ w ⁡ N = X
10 df-ne ⊢ w ⁡ N ≠ X ↔ ¬ w ⁡ N = X
11 wwlknlsw ⊢ w ∈ N WWalksN G → w ⁡ N = lastS ⁡ w
12 11 neeq1d ⊢ w ∈ N WWalksN G → w ⁡ N ≠ X ↔ lastS ⁡ w ≠ X
13 10 12 bitr3id ⊢ w ∈ N WWalksN G → ¬ w ⁡ N = X ↔ lastS ⁡ w ≠ X
14 13 anbi2d ⊢ w ∈ N WWalksN G → w ⁡ 0 = X ∧ ¬ w ⁡ N = X ↔ w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
15 9 14 bitrid ⊢ w ∈ N WWalksN G → w ⁡ 0 = X ∧ ¬ w ⁡ 0 = X ∧ w ⁡ N = X ↔ w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
16 15 rabbiia ⊢ w ∈ N WWalksN G | w ⁡ 0 = X ∧ ¬ w ⁡ 0 = X ∧ w ⁡ N = X = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
17 7 8 16 3eqtrri ⊢ w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X = C ∖ B
18 1 17 eqtri ⊢ A = C ∖ B