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 = ( Vtx ` G )
Assertion	clnbgrvtxel	|- ( K e. V -> K e. ( G ClNeighbVtx K ) )

Proof

Step	Hyp	Ref	Expression
1		clnbgrvtxel.v	|- V = ( Vtx ` G )
2		id	|- ( K e. V -> K e. V )
3		eqidd	|- ( K e. V -> K = K )
4	3	orcd	|- ( K e. V -> ( K = K \/ E. e e. ( Edg ` G ) { K , K } C_ e ) )
5		eqid	|- ( Edg ` G ) = ( Edg ` G )
6	1 5	clnbgrel	|- ( K e. ( G ClNeighbVtx K ) <-> ( ( K e. V /\ K e. V ) /\ ( K = K \/ E. e e. ( Edg ` G ) { K , K } C_ e ) ) )
7	2 2 4 6	syl21anbrc	|- ( K e. V -> K e. ( G ClNeighbVtx K ) )