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 e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
	clwwlknclwwlkdif.b	|- B = ( X ( N WWalksNOn G ) X )
	clwwlknclwwlkdif.c	|- C = { w e. ( N WWalksN G ) | ( w ` 0 ) = X }
Assertion	clwwlknclwwlkdif	|- A = ( C \ B )

Proof

Step	Hyp	Ref	Expression
1		clwwlknclwwlkdif.a	|- A = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
2		clwwlknclwwlkdif.b	|- B = ( X ( N WWalksNOn G ) X )
3		clwwlknclwwlkdif.c	|- C = { w e. ( N WWalksN G ) | ( w ` 0 ) = X }
4		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
5	4	iswwlksnon	|- ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) }
6	2 5	eqtri	|- B = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) }
7	3 6	difeq12i	|- ( C \ B ) = ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) } )
8		difrab	|- ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) } ) = { w e. ( 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 e. ( N WWalksN G ) -> ( w ` N ) = ( lastS ` w ) )
12	11	neeq1d	|- ( w e. ( N WWalksN G ) -> ( ( w ` N ) =/= X <-> ( lastS ` w ) =/= X ) )
13	10 12	bitr3id	|- ( w e. ( N WWalksN G ) -> ( -. ( w ` N ) = X <-> ( lastS ` w ) =/= X ) )
14	13	anbi2d	|- ( w e. ( N WWalksN G ) -> ( ( ( w ` 0 ) = X /\ -. ( w ` N ) = X ) <-> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
15	9 14	syl5bb	|- ( w e. ( N WWalksN G ) -> ( ( ( w ` 0 ) = X /\ -. ( ( w ` 0 ) = X /\ ( w ` N ) = X ) ) <-> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
16	15	rabbiia	|- { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ -. ( ( w ` 0 ) = X /\ ( w ` N ) = X ) ) } = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
17	7 8 16	3eqtrri	|- { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } = ( C \ B )
18	1 17	eqtri	|- A = ( C \ B )