Step |
Hyp |
Ref |
Expression |
1 |
|
uspgrloopvtx.g |
|- G = <. V , { <. A , { N } >. } >. |
2 |
1
|
uspgrloopvtx |
|- ( V e. W -> ( Vtx ` G ) = V ) |
3 |
2
|
3ad2ant1 |
|- ( ( V e. W /\ A e. X /\ N e. V ) -> ( Vtx ` G ) = V ) |
4 |
|
simp2 |
|- ( ( V e. W /\ A e. X /\ N e. V ) -> A e. X ) |
5 |
|
simp3 |
|- ( ( V e. W /\ A e. X /\ N e. V ) -> N e. V ) |
6 |
1
|
uspgrloopiedg |
|- ( ( V e. W /\ A e. X ) -> ( iEdg ` G ) = { <. A , { N } >. } ) |
7 |
6
|
3adant3 |
|- ( ( V e. W /\ A e. X /\ N e. V ) -> ( iEdg ` G ) = { <. A , { N } >. } ) |
8 |
3 4 5 7
|
1loopgrnb0 |
|- ( ( V e. W /\ A e. X /\ N e. V ) -> ( G NeighbVtx N ) = (/) ) |