Metamath Proof Explorer


Theorem clnbgrvtxel

Description: Every vertex K is a member of its closed neighborhood. (Contributed by AV, 10-May-2025)

Ref Expression
Hypothesis clnbgrvtxel.v V=VtxG
Assertion clnbgrvtxel Could not format assertion : No typesetting found for |- ( K e. V -> K e. ( G ClNeighbVtx K ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 clnbgrvtxel.v V=VtxG
2 id KVKV
3 eqidd KVK=K
4 3 orcd KVK=KeEdgGKKe
5 eqid EdgG=EdgG
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 |-