Theorem dfnbgrss2

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

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

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	|- V = ( Vtx ` G )
2		dfvopnbgr2.e	|- E = ( Edg ` G )
3		dfvopnbgr2.u	|- U = { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
4		dfsclnbgr6.s	|- S = { n e. V | E. e e. E { N , n } C_ e }
5	1 2 3	dfnbgr6	|- ( N e. V -> ( G NeighbVtx N ) = ( U \ { N } ) )
6		difss	|- ( U \ { N } ) C_ U
7	5 6	eqsstrdi	|- ( N e. V -> ( G NeighbVtx N ) C_ U )
8		ssun1	|- U C_ ( U u. { n e. { N } | E. e e. E n e. e } )
9	1 2 3 4	dfsclnbgr6	|- ( N e. V -> S = ( U u. { n e. { N } | E. e e. E n e. e } ) )
10	8 9	sseqtrrid	|- ( N e. V -> U C_ S )
11	1 4 2	dfnbgrss	|- ( N e. V -> ( ( G NeighbVtx N ) C_ S /\ S C_ ( G ClNeighbVtx N ) ) )
12	11	simprd	|- ( N e. V -> S C_ ( G ClNeighbVtx N ) )
13	7 10 12	3jca	|- ( N e. V -> ( ( G NeighbVtx N ) C_ U /\ U C_ S /\ S C_ ( G ClNeighbVtx N ) ) )