Theorem sclnbgrelself

Description: A vertex N is a member of its semiclosed neighborhood iff there is an edge joining the vertex with a vertex. (Contributed by AV, 16-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
3		dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4	1 2 3	sclnbgrel	⊢ ( 𝑁 ∈ 𝑆 ↔ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑁 } ⊆ 𝑒 ) )
5		dfsn2	⊢ { 𝑁 } = { 𝑁 , 𝑁 }
6	5	eqcomi	⊢ { 𝑁 , 𝑁 } = { 𝑁 }
7	6	sseq1i	⊢ ( { 𝑁 , 𝑁 } ⊆ 𝑒 ↔ { 𝑁 } ⊆ 𝑒 )
8		snssg	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ 𝑒 ↔ { 𝑁 } ⊆ 𝑒 ) )
9	7 8	bitr4id	⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 , 𝑁 } ⊆ 𝑒 ↔ 𝑁 ∈ 𝑒 ) )
10	9	rexbidv	⊢ ( 𝑁 ∈ 𝑉 → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑁 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 𝑁 ∈ 𝑒 ) )
11	10	pm5.32i	⊢ ( ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑁 } ⊆ 𝑒 ) ↔ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 𝑁 ∈ 𝑒 ) )
12	4 11	bitri	⊢ ( 𝑁 ∈ 𝑆 ↔ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 𝑁 ∈ 𝑒 ) )