Theorem dfnbgrss2

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

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

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfvopnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		dfvopnbgr2.u	⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
4		dfsclnbgr6.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
5	1 2 3	dfnbgr6	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑈 ∖ { 𝑁 } ) )
6		difss	⊢ ( 𝑈 ∖ { 𝑁 } ) ⊆ 𝑈
7	5 6	eqsstrdi	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) ⊆ 𝑈 )
8		ssun1	⊢ 𝑈 ⊆ ( 𝑈 ∪ { 𝑛 ∈ { 𝑁 } ∣ ∃ 𝑒 ∈ 𝐸 𝑛 ∈ 𝑒 } )
9	1 2 3 4	dfsclnbgr6	⊢ ( 𝑁 ∈ 𝑉 → 𝑆 = ( 𝑈 ∪ { 𝑛 ∈ { 𝑁 } ∣ ∃ 𝑒 ∈ 𝐸 𝑛 ∈ 𝑒 } ) )
10	8 9	sseqtrrid	⊢ ( 𝑁 ∈ 𝑉 → 𝑈 ⊆ 𝑆 )
11	1 4 2	dfnbgrss	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝐺 NeighbVtx 𝑁 ) ⊆ 𝑆 ∧ 𝑆 ⊆ ( 𝐺 ClNeighbVtx 𝑁 ) ) )
12	11	simprd	⊢ ( 𝑁 ∈ 𝑉 → 𝑆 ⊆ ( 𝐺 ClNeighbVtx 𝑁 ) )
13	7 10 12	3jca	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝐺 NeighbVtx 𝑁 ) ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑆 ∧ 𝑆 ⊆ ( 𝐺 ClNeighbVtx 𝑁 ) ) )