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	⊢ 𝐴 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) }
	clwwlknclwwlkdif.b	⊢ 𝐵 = ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 )
	clwwlknclwwlkdif.c	⊢ 𝐶 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
Assertion	clwwlknclwwlkdif	⊢ 𝐴 = ( 𝐶 ∖ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		clwwlknclwwlkdif.a	⊢ 𝐴 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) }
2		clwwlknclwwlkdif.b	⊢ 𝐵 = ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 )
3		clwwlknclwwlkdif.c	⊢ 𝐶 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
4		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5	4	iswwlksnon	⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) }
6	2 5	eqtri	⊢ 𝐵 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) }
7	3 6	difeq12i	⊢ ( 𝐶 ∖ 𝐵 ) = ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) } )
8		difrab	⊢ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∖ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) } ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ¬ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ) }
9		annotanannot	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ¬ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ¬ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) )
10		df-ne	⊢ ( ( 𝑤 ‘ 𝑁 ) ≠ 𝑋 ↔ ¬ ( 𝑤 ‘ 𝑁 ) = 𝑋 )
11		wwlknlsw	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑤 ‘ 𝑁 ) = ( lastS ‘ 𝑤 ) )
12	11	neeq1d	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑤 ‘ 𝑁 ) ≠ 𝑋 ↔ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) )
13	10 12	bitr3id	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ¬ ( 𝑤 ‘ 𝑁 ) = 𝑋 ↔ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) )
14	13	anbi2d	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ¬ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) ) )
15	9 14	syl5bb	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ¬ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) ) )
16	15	rabbiia	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ¬ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) }
17	7 8 16	3eqtrri	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } = ( 𝐶 ∖ 𝐵 )
18	1 17	eqtri	⊢ 𝐴 = ( 𝐶 ∖ 𝐵 )