This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nbgrssvwo2

Description: The neighbors of a vertex X form a subset of all vertices except the vertex X itself and a class M which is not a neighbor of X . (Contributed by Alexander van der Vekens, 13-Jul-2018) (Revised by AV, 3-Nov-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypothesis nbgrssovtx.v ⊢ V = Vtx ⁡ G
Assertion nbgrssvwo2 ⊢ M ∉ G NeighbVtx X → G NeighbVtx X ⊆ V ∖ M X

Proof

Step Hyp Ref Expression
1 nbgrssovtx.v ⊢ V = Vtx ⁡ G
2 1 nbgrssovtx ⊢ G NeighbVtx X ⊆ V ∖ X
3 df-nel ⊢ M ∉ G NeighbVtx X ↔ ¬ M ∈ G NeighbVtx X
4 disjsn ⊢ G NeighbVtx X ∩ M = ∅ ↔ ¬ M ∈ G NeighbVtx X
5 3 4 sylbb2 ⊢ M ∉ G NeighbVtx X → G NeighbVtx X ∩ M = ∅
6 reldisj ⊢ G NeighbVtx X ⊆ V ∖ X → G NeighbVtx X ∩ M = ∅ ↔ G NeighbVtx X ⊆ V ∖ X ∖ M
7 5 6 imbitrid ⊢ G NeighbVtx X ⊆ V ∖ X → M ∉ G NeighbVtx X → G NeighbVtx X ⊆ V ∖ X ∖ M
8 2 7 ax-mp ⊢ M ∉ G NeighbVtx X → G NeighbVtx X ⊆ V ∖ X ∖ M
9 prcom ⊢ M X = X M
10 9 difeq2i ⊢ V ∖ M X = V ∖ X M
11 difpr ⊢ V ∖ X M = V ∖ X ∖ M
12 10 11 eqtri ⊢ V ∖ M X = V ∖ X ∖ M
13 8 12 sseqtrrdi ⊢ M ∉ G NeighbVtx X → G NeighbVtx X ⊆ V ∖ M X