| Step |
Hyp |
Ref |
Expression |
| 1 |
|
usgrexmpl2.v |
|- V = ( 0 ... 5 ) |
| 2 |
|
usgrexmpl2.e |
|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> |
| 3 |
|
usgrexmpl2.g |
|- G = <. V , E >. |
| 4 |
1 2 3
|
usgrexmpl2 |
|- G e. USGraph |
| 5 |
1 2 3
|
usgrexmpl2vtx |
|- ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) |
| 6 |
5
|
eqcomi |
|- ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) = ( Vtx ` G ) |
| 7 |
1 2 3
|
usgrexmpl2edg |
|- ( Edg ` G ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) |
| 8 |
7
|
eqcomi |
|- ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) = ( Edg ` G ) |
| 9 |
6 8
|
nbusgrvtx |
|- ( ( G e. USGraph /\ K e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) -> ( G NeighbVtx K ) = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { K , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } ) |
| 10 |
4 9
|
mpan |
|- ( K e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) -> ( G NeighbVtx K ) = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { K , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } ) |