Theorem clwwlknclwwlkdifs 26873

Description: The set of walks of length n starting with a fixed vertex and ending not at this vertex is the difference between the set of walks of length n starting with this vertex and the set of walks of length n starting with this vertex and ending at this vertex. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.)

Hypotheses

Ref	Expression
clwwlknclwwlkdif.a	|- A = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
clwwlknclwwlkdif.b	|- B = { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) }

Assertion

Ref	Expression
clwwlknclwwlkdifs	|- A = ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B )

Proof of Theorem clwwlknclwwlkdifs

Step	Hyp	Ref	Expression
1		clwwlknclwwlkdif.a	. 2 |- A = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
2		clwwlknclwwlkdif.b	. . . 4 |- B = { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) }
3	2	difeq2i 3725	. . 3 |- ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B ) = ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } )
4		difrab 3901	. . 3 |- ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) }
5		ianor 509	. . . . . . . 8 |- ( -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) <-> ( -. ( lastS ` w ) = ( w ` 0 ) \/ -. ( w ` 0 ) = X ) )
6		eqeq2 2633	. . . . . . . . . . . 12 |- ( ( w ` 0 ) = X -> ( ( lastS ` w ) = ( w ` 0 ) <-> ( lastS ` w ) = X ) )
7	6	notbid 308	. . . . . . . . . . 11 |- ( ( w ` 0 ) = X -> ( -. ( lastS ` w ) = ( w ` 0 ) <-> -. ( lastS ` w ) = X ) )
8		neqne 2802	. . . . . . . . . . . . 13 |- ( -. ( lastS ` w ) = X -> ( lastS ` w ) =/= X )
9	8	anim2i 593	. . . . . . . . . . . 12 |- ( ( ( w ` 0 ) = X /\ -. ( lastS ` w ) = X ) -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) )
10	9	ex 450	. . . . . . . . . . 11 |- ( ( w ` 0 ) = X -> ( -. ( lastS ` w ) = X -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
11	7, 10	sylbid 230	. . . . . . . . . 10 |- ( ( w ` 0 ) = X -> ( -. ( lastS ` w ) = ( w ` 0 ) -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
12	11	com12 32	. . . . . . . . 9 |- ( -. ( lastS ` w ) = ( w ` 0 ) -> ( ( w ` 0 ) = X -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
13		pm2.21 120	. . . . . . . . 9 |- ( -. ( w ` 0 ) = X -> ( ( w ` 0 ) = X -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
14	12, 13	jaoi 394	. . . . . . . 8 |- ( ( -. ( lastS ` w ) = ( w ` 0 ) \/ -. ( w ` 0 ) = X ) -> ( ( w ` 0 ) = X -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
15	5, 14	sylbi 207	. . . . . . 7 |- ( -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) -> ( ( w ` 0 ) = X -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
16	15	impcom 446	. . . . . 6 |- ( ( ( w ` 0 ) = X /\ -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) -> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) )
17		simpl 473	. . . . . . 7 |- ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) -> ( w ` 0 ) = X )
18		neeq2 2857	. . . . . . . . . . 11 |- ( X = ( w ` 0 ) -> ( ( lastS ` w ) =/= X <-> ( lastS ` w ) =/= ( w ` 0 ) ) )
19	18	eqcoms 2630	. . . . . . . . . 10 |- ( ( w ` 0 ) = X -> ( ( lastS ` w ) =/= X <-> ( lastS ` w ) =/= ( w ` 0 ) ) )
20		neneq 2800	. . . . . . . . . 10 |- ( ( lastS ` w ) =/= ( w ` 0 ) -> -. ( lastS ` w ) = ( w ` 0 ) )
21	19, 20	syl6bi 243	. . . . . . . . 9 |- ( ( w ` 0 ) = X -> ( ( lastS ` w ) =/= X -> -. ( lastS ` w ) = ( w ` 0 ) ) )
22	21	imp 445	. . . . . . . 8 |- ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) -> -. ( lastS ` w ) = ( w ` 0 ) )
23	22	intnanrd 963	. . . . . . 7 |- ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) -> -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) )
24	17, 23	jca 554	. . . . . 6 |- ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) -> ( ( w ` 0 ) = X /\ -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) )
25	16, 24	impbii 199	. . . . 5 |- ( ( ( w ` 0 ) = X /\ -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) <-> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) )
26	25	a1i 11	. . . 4 |- ( w e. ( N WWalksN G ) -> ( ( ( w ` 0 ) = X /\ -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) <-> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
27	26	rabbiia 3185	. . 3 |- { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ -. ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) } = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
28	3, 4, 27	3eqtrri 2649	. 2 |- { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } = ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B )
29	1, 28	eqtri 2644	1 |- A = ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   {crab 2916   \ cdif 3571   ` cfv 5888  (class class class)co 6650   0cc0 9936   lastS clsw 13292   WWalksN cwwlksn 26718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577

This theorem is referenced by:  clwwlknclwwlkdifnum  26874