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