This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjxwwlksn

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, 29-Jul-2018) (Revised by AV, 19-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnexthasheq.v 
|- V = ( Vtx ` G )
wwlksnexthasheq.e 
|- E = ( Edg ` G )
Assertion disjxwwlksn 
|- Disj_ y e. ( N WWalksN G ) { x e. Word V | ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) }

Proof

Step Hyp Ref Expression
1 wwlksnexthasheq.v 
 |-  V = ( Vtx ` G )
2 wwlksnexthasheq.e 
 |-  E = ( Edg ` G )
3 simp1 
 |-  ( ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x prefix N ) = y )
4 3 a1i 
 |-  ( x e. Word V -> ( ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x prefix N ) = y ) )
5 4 ss2rabi 
 |-  { x e. Word V | ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. Word V | ( x prefix N ) = y }
6 5 rgenw 
 |-  A. y e. ( N WWalksN G ) { x e. Word V | ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. Word V | ( x prefix N ) = y }
7 disjwrdpfx 
 |-  Disj_ y e. ( N WWalksN G ) { x e. Word V | ( x prefix N ) = y }
8 disjss2 
 |-  ( A. y e. ( N WWalksN G ) { x e. Word V | ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. Word V | ( x prefix N ) = y } -> ( Disj_ y e. ( N WWalksN G ) { x e. Word V | ( x prefix N ) = y } -> Disj_ y e. ( N WWalksN G ) { x e. Word V | ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) )
9 6 7 8 mp2 
 |-  Disj_ y e. ( N WWalksN G ) { x e. Word V | ( ( x prefix N ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) }