Step |
Hyp |
Ref |
Expression |
1 |
|
nbgrssovtx.v |
|- V = ( Vtx ` G ) |
2 |
1
|
nbgrssovtx |
|- ( G NeighbVtx X ) C_ ( V \ { X } ) |
3 |
|
df-nel |
|- ( M e/ ( G NeighbVtx X ) <-> -. M e. ( G NeighbVtx X ) ) |
4 |
|
disjsn |
|- ( ( ( G NeighbVtx X ) i^i { M } ) = (/) <-> -. M e. ( G NeighbVtx X ) ) |
5 |
3 4
|
sylbb2 |
|- ( M e/ ( G NeighbVtx X ) -> ( ( G NeighbVtx X ) i^i { M } ) = (/) ) |
6 |
|
reldisj |
|- ( ( G NeighbVtx X ) C_ ( V \ { X } ) -> ( ( ( G NeighbVtx X ) i^i { M } ) = (/) <-> ( G NeighbVtx X ) C_ ( ( V \ { X } ) \ { M } ) ) ) |
7 |
5 6
|
syl5ib |
|- ( ( G NeighbVtx X ) C_ ( V \ { X } ) -> ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( ( V \ { X } ) \ { M } ) ) ) |
8 |
2 7
|
ax-mp |
|- ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( ( V \ { X } ) \ { M } ) ) |
9 |
|
prcom |
|- { M , X } = { X , M } |
10 |
9
|
difeq2i |
|- ( V \ { M , X } ) = ( V \ { X , M } ) |
11 |
|
difpr |
|- ( V \ { X , M } ) = ( ( V \ { X } ) \ { M } ) |
12 |
10 11
|
eqtri |
|- ( V \ { M , X } ) = ( ( V \ { X } ) \ { M } ) |
13 |
8 12
|
sseqtrrdi |
|- ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( V \ { M , X } ) ) |