Metamath Proof Explorer

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 ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
dfsclnbgr6.s ⊢ S = n ∈ V | ∃ e ∈ E N n ⊆ e
Assertion dfnbgrss2 ⊢ N ∈ V → G NeighbVtx N ⊆ U ∧ U ⊆ S ∧ S ⊆ 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 ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
4 dfsclnbgr6.s ⊢ S = n ∈ V | ∃ e ∈ E N n ⊆ e
5 1 2 3 dfnbgr6 ⊢ N ∈ V → G NeighbVtx N = U ∖ N
6 difss ⊢ U ∖ N ⊆ U
7 5 6 eqsstrdi ⊢ N ∈ V → G NeighbVtx N ⊆ U
8 ssun1 ⊢ U ⊆ U ∪ n ∈ N | ∃ e ∈ E n ∈ e
9 1 2 3 4 dfsclnbgr6 ⊢ N ∈ V → S = U ∪ n ∈ N | ∃ e ∈ E n ∈ e
10 8 9 sseqtrrid ⊢ N ∈ V → U ⊆ S
11 1 4 2 dfnbgrss ⊢ N ∈ V → G NeighbVtx N ⊆ S ∧ S ⊆ G ClNeighbVtx N
12 11 simprd ⊢ N ∈ V → S ⊆ G ClNeighbVtx N
13 7 10 12 3jca ⊢ N ∈ V → G NeighbVtx N ⊆ U ∧ U ⊆ S ∧ S ⊆ G ClNeighbVtx N