Theorem dfnbgrss

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

	Ref	Expression
Hypotheses	dfsclnbgr2.v	|- V = ( Vtx ` G )
	dfsclnbgr2.s	|- S = { n e. V | E. e e. E { N , n } C_ e }
	dfsclnbgr2.e	|- E = ( Edg ` G )
Assertion	dfnbgrss	|- ( N e. V -> ( ( G NeighbVtx N ) C_ S /\ S C_ ( G ClNeighbVtx N ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	|- V = ( Vtx ` G )
2		dfsclnbgr2.s	|- S = { n e. V | E. e e. E { N , n } C_ e }
3		dfsclnbgr2.e	|- E = ( Edg ` G )
4	1 2 3	dfnbgr5	|- ( N e. V -> ( G NeighbVtx N ) = ( S \ { N } ) )
5		difss	|- ( S \ { N } ) C_ S
6	4 5	eqsstrdi	|- ( N e. V -> ( G NeighbVtx N ) C_ S )
7		ssun2	|- S C_ ( { N } u. S )
8	1 2 3	dfclnbgr5	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. S ) )
9	7 8	sseqtrrid	|- ( N e. V -> S C_ ( G ClNeighbVtx N ) )
10	6 9	jca	|- ( N e. V -> ( ( G NeighbVtx N ) C_ S /\ S C_ ( G ClNeighbVtx N ) ) )