Theorem clnbgrvtxel

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

	Ref	Expression
Hypothesis	clnbgrvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	clnbgrvtxel	⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		clnbgrvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		id	⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ 𝑉 )
3		eqidd	⊢ ( 𝐾 ∈ 𝑉 → 𝐾 = 𝐾 )
4	3	orcd	⊢ ( 𝐾 ∈ 𝑉 → ( 𝐾 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝐾 } ⊆ 𝑒 ) )
5		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
6	1 5	clnbgrel	⊢ ( 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( ( 𝐾 ∈ 𝑉 ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝐾 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝐾 } ⊆ 𝑒 ) ) )
7	2 2 4 6	syl21anbrc	⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) )