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	syl5ib	⊢ ( ( 𝐺 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 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑀 , 𝑋 } ) )