Theorem sclnbgrisvtx

Description: Every member X of the semiclosed neighborhood of a vertex N is a vertex. (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
	dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	sclnbgrisvtx	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
3		dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4	1 2 3	sclnbgrel	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑋 } ⊆ 𝑒 ) )
5	4	simplbi	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉 )