Theorem dfnbgrss

Description: Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
3		dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4	1 2 3	dfnbgr5	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑆 ∖ { 𝑁 } ) )
5		difss	⊢ ( 𝑆 ∖ { 𝑁 } ) ⊆ 𝑆
6	4 5	eqsstrdi	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) ⊆ 𝑆 )
7		ssun2	⊢ 𝑆 ⊆ ( { 𝑁 } ∪ 𝑆 )
8	1 2 3	dfclnbgr5	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ 𝑆 ) )
9	7 8	sseqtrrid	⊢ ( 𝑁 ∈ 𝑉 → 𝑆 ⊆ ( 𝐺 ClNeighbVtx 𝑁 ) )
10	6 9	jca	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝐺 NeighbVtx 𝑁 ) ⊆ 𝑆 ∧ 𝑆 ⊆ ( 𝐺 ClNeighbVtx 𝑁 ) ) )