| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
| 2 |
1
|
clnbgrcl |
|- ( X e. ( G ClNeighbVtx N ) -> N e. ( Vtx ` G ) ) |
| 3 |
1
|
dfclnbgr4 |
|- ( N e. ( Vtx ` G ) -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) |
| 4 |
2 3
|
syl |
|- ( X e. ( G ClNeighbVtx N ) -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) |
| 5 |
4
|
eleq2d |
|- ( X e. ( G ClNeighbVtx N ) -> ( X e. ( G ClNeighbVtx N ) <-> X e. ( { N } u. ( G NeighbVtx N ) ) ) ) |
| 6 |
|
elun |
|- ( X e. ( { N } u. ( G NeighbVtx N ) ) <-> ( X e. { N } \/ X e. ( G NeighbVtx N ) ) ) |
| 7 |
|
elsng |
|- ( X e. ( G ClNeighbVtx N ) -> ( X e. { N } <-> X = N ) ) |
| 8 |
|
eqneqall |
|- ( X = N -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) |
| 9 |
8
|
a1i |
|- ( X e. ( G ClNeighbVtx N ) -> ( X = N -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) ) |
| 10 |
7 9
|
sylbid |
|- ( X e. ( G ClNeighbVtx N ) -> ( X e. { N } -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) ) |
| 11 |
|
ax-1 |
|- ( X e. ( G NeighbVtx N ) -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) |
| 12 |
11
|
a1i |
|- ( X e. ( G ClNeighbVtx N ) -> ( X e. ( G NeighbVtx N ) -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) ) |
| 13 |
10 12
|
jaod |
|- ( X e. ( G ClNeighbVtx N ) -> ( ( X e. { N } \/ X e. ( G NeighbVtx N ) ) -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) ) |
| 14 |
6 13
|
biimtrid |
|- ( X e. ( G ClNeighbVtx N ) -> ( X e. ( { N } u. ( G NeighbVtx N ) ) -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) ) |
| 15 |
5 14
|
sylbid |
|- ( X e. ( G ClNeighbVtx N ) -> ( X e. ( G ClNeighbVtx N ) -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) ) |
| 16 |
15
|
pm2.43i |
|- ( X e. ( G ClNeighbVtx N ) -> ( X =/= N -> X e. ( G NeighbVtx N ) ) ) |
| 17 |
16
|
imp |
|- ( ( X e. ( G ClNeighbVtx N ) /\ X =/= N ) -> X e. ( G NeighbVtx N ) ) |