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 ) ) |