Theorem disjxwwlkn

Description: Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 26-Oct-2022)

	Ref	Expression
Hypotheses	wwlksnextprop.x	|- X = ( ( N + 1 ) WWalksN G )
	wwlksnextprop.e	|- E = ( Edg ` G )
	wwlksnextprop.y	|- Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
Assertion	disjxwwlkn	|- Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) }

Proof

Step	Hyp	Ref	Expression
1		wwlksnextprop.x	|- X = ( ( N + 1 ) WWalksN G )
2		wwlksnextprop.e	|- E = ( Edg ` G )
3		wwlksnextprop.y	|- Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
4		simp1	|- ( ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x prefix M ) = y )
5	4	a1i	|- ( x e. X -> ( ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x prefix M ) = y ) )
6	5	ss2rabi	|- { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. X | ( x prefix M ) = y }
7		wwlkssswwlksn	|- ( ( N + 1 ) WWalksN G ) C_ ( WWalks ` G )
8		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
9	8	wwlkssswrd	|- ( WWalks ` G ) C_ Word ( Vtx ` G )
10	7 9	sstri	|- ( ( N + 1 ) WWalksN G ) C_ Word ( Vtx ` G )
11	1 10	eqsstri	|- X C_ Word ( Vtx ` G )
12		rabss2	|- ( X C_ Word ( Vtx ` G ) -> { x e. X | ( x prefix M ) = y } C_ { x e. Word ( Vtx ` G ) | ( x prefix M ) = y } )
13	11 12	ax-mp	|- { x e. X | ( x prefix M ) = y } C_ { x e. Word ( Vtx ` G ) | ( x prefix M ) = y }
14	6 13	sstri	|- { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. Word ( Vtx ` G ) | ( x prefix M ) = y }
15	14	rgenw	|- A. y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. Word ( Vtx ` G ) | ( x prefix M ) = y }
16		disjwrdpfx	|- Disj_ y e. Y { x e. Word ( Vtx ` G ) | ( x prefix M ) = y }
17		disjss2	|- ( A. y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. Word ( Vtx ` G ) | ( x prefix M ) = y } -> ( Disj_ y e. Y { x e. Word ( Vtx ` G ) | ( x prefix M ) = y } -> Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) )
18	15 16 17	mp2	|- Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) }