Description: Every vertex K is a member of its closed neighborhood. (Contributed by AV, 10-May-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | clnbgrvtxel.v | |
|
Assertion | clnbgrvtxel | Could not format assertion : No typesetting found for |- ( K e. V -> K e. ( G ClNeighbVtx K ) ) with typecode |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clnbgrvtxel.v | |
|
2 | id | |
|
3 | eqidd | |
|
4 | 3 | orcd | |
5 | eqid | |
|
6 | 1 5 | clnbgrel | Could not format ( K e. ( G ClNeighbVtx K ) <-> ( ( K e. V /\ K e. V ) /\ ( K = K \/ E. e e. ( Edg ` G ) { K , K } C_ e ) ) ) : No typesetting found for |- ( K e. ( G ClNeighbVtx K ) <-> ( ( K e. V /\ K e. V ) /\ ( K = K \/ E. e e. ( Edg ` G ) { K , K } C_ e ) ) ) with typecode |- |
7 | 2 2 4 6 | syl21anbrc | Could not format ( K e. V -> K e. ( G ClNeighbVtx K ) ) : No typesetting found for |- ( K e. V -> K e. ( G ClNeighbVtx K ) ) with typecode |- |