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 |
|
wwlksnfi |
|- ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) |
5 |
|
ssrab2 |
|- { w e. ( N WWalksN G ) | ( w ` 0 ) = P } C_ ( N WWalksN G ) |
6 |
|
ssfi |
|- ( ( ( N WWalksN G ) e. Fin /\ { w e. ( N WWalksN G ) | ( w ` 0 ) = P } C_ ( N WWalksN G ) ) -> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } e. Fin ) |
7 |
4 5 6
|
sylancl |
|- ( ( Vtx ` G ) e. Fin -> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } e. Fin ) |
8 |
3 7
|
eqeltrid |
|- ( ( Vtx ` G ) e. Fin -> Y e. Fin ) |
9 |
|
wwlksnfi |
|- ( ( Vtx ` G ) e. Fin -> ( ( N + 1 ) WWalksN G ) e. Fin ) |
10 |
1 9
|
eqeltrid |
|- ( ( Vtx ` G ) e. Fin -> X e. Fin ) |
11 |
|
rabfi |
|- ( X e. Fin -> { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } e. Fin ) |
12 |
10 11
|
syl |
|- ( ( Vtx ` G ) e. Fin -> { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } e. Fin ) |
13 |
12
|
adantr |
|- ( ( ( Vtx ` G ) e. Fin /\ y e. Y ) -> { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } e. Fin ) |
14 |
1 2 3
|
disjxwwlkn |
|- Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } |
15 |
14
|
a1i |
|- ( ( Vtx ` G ) e. Fin -> Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) |
16 |
8 13 15
|
hashrabrex |
|- ( ( Vtx ` G ) e. Fin -> ( # ` { x e. X | E. y e. Y ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) = sum_ y e. Y ( # ` { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) ) |