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

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 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 ) }