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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion nbgrssvwo2 ( 𝑀 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑀 , 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 nbgrssovtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 nbgrssovtx ⊢ ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑋 } )
3 df-nel ⊢ ( 𝑀 ∉ ( 𝐺 NeighbVtx 𝑋 ) ↔ ¬ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
4 disjsn ⊢ ( ( ( 𝐺 NeighbVtx 𝑋 ) ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
5 3 4 sylbb2 ⊢ ( 𝑀 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝐺 NeighbVtx 𝑋 ) ∩ { 𝑀 } ) = ∅ )
6 reldisj ⊢ ( ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑋 } ) → ( ( ( 𝐺 NeighbVtx 𝑋 ) ∩ { 𝑀 } ) = ∅ ↔ ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( ( 𝑉 ∖ { 𝑋 } ) ∖ { 𝑀 } ) ) )
7 5 6 imbitrid ⊢ ( ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑋 } ) → ( 𝑀 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( ( 𝑉 ∖ { 𝑋 } ) ∖ { 𝑀 } ) ) )
8 2 7 ax-mp ⊢ ( 𝑀 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( ( 𝑉 ∖ { 𝑋 } ) ∖ { 𝑀 } ) )
9 prcom ⊢ { 𝑀 , 𝑋 } = { 𝑋 , 𝑀 }
10 9 difeq2i ⊢ ( 𝑉 ∖ { 𝑀 , 𝑋 } ) = ( 𝑉 ∖ { 𝑋 , 𝑀 } )
11 difpr ⊢ ( 𝑉 ∖ { 𝑋 , 𝑀 } ) = ( ( 𝑉 ∖ { 𝑋 } ) ∖ { 𝑀 } )
12 10 11 eqtri ⊢ ( 𝑉 ∖ { 𝑀 , 𝑋 } ) = ( ( 𝑉 ∖ { 𝑋 } ) ∖ { 𝑀 } )
13 8 12 sseqtrrdi ⊢ ( 𝑀 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑀 , 𝑋 } ) )