Step |
Hyp |
Ref |
Expression |
1 |
|
frgrhash2wsp.v |
|- V = ( Vtx ` G ) |
2 |
|
fusgreg2wsp.m |
|- M = ( a e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } ) |
3 |
|
eqeq2 |
|- ( a = N -> ( ( w ` 1 ) = a <-> ( w ` 1 ) = N ) ) |
4 |
3
|
rabbidv |
|- ( a = N -> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } = { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } ) |
5 |
|
ovex |
|- ( 2 WSPathsN G ) e. _V |
6 |
5
|
rabex |
|- { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } e. _V |
7 |
4 2 6
|
fvmpt |
|- ( N e. V -> ( M ` N ) = { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } ) |
8 |
7
|
eleq2d |
|- ( N e. V -> ( p e. ( M ` N ) <-> p e. { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } ) ) |
9 |
|
fveq1 |
|- ( w = p -> ( w ` 1 ) = ( p ` 1 ) ) |
10 |
9
|
eqeq1d |
|- ( w = p -> ( ( w ` 1 ) = N <-> ( p ` 1 ) = N ) ) |
11 |
10
|
elrab |
|- ( p e. { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } <-> ( p e. ( 2 WSPathsN G ) /\ ( p ` 1 ) = N ) ) |
12 |
8 11
|
syl6bb |
|- ( N e. V -> ( p e. ( M ` N ) <-> ( p e. ( 2 WSPathsN G ) /\ ( p ` 1 ) = N ) ) ) |