Metamath Proof Explorer

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 rgenw 
 |-  A. x e. X ( ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x prefix M ) = y )
6 ss2rab 
 |-  ( { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. X | ( x prefix M ) = y } <-> A. x e. X ( ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x prefix M ) = y ) )
7 5 6 mpbir 
 |-  { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } C_ { x e. X | ( x prefix M ) = y }
8 wwlkssswwlksn 
 |-  ( ( N + 1 ) WWalksN G ) C_ ( WWalks ` G )
9 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
10 9 wwlkssswrd 
 |-  ( WWalks ` G ) C_ Word ( Vtx ` G )
11 8 10 sstri 
 |-  ( ( N + 1 ) WWalksN G ) C_ Word ( Vtx ` G )
12 1 11 eqsstri 
 |-  X C_ Word ( Vtx ` G )
13 rabss2 
 |-  ( X C_ Word ( Vtx ` G ) -> { x e. X | ( x prefix M ) = y } C_ { x e. Word ( Vtx ` G ) | ( x prefix M ) = y } )
14 12 13 ax-mp 
 |-  { x e. X | ( x prefix M ) = y } C_ { x e. Word ( Vtx ` G ) | ( x prefix M ) = y }
15 7 14 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 }
16 15 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 }
17 disjwrdpfx 
 |-  Disj_ y e. Y { x e. Word ( Vtx ` G ) | ( x prefix M ) = y }
18 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 ) } ) )
19 16 17 18 mp2 
 |-  Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) }