Theorem nbgrssovtx

Description: The neighbors of a vertex X form a subset of all vertices except the vertex X itself. Stronger version of nbgrssvtx . (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	nbgrssovtx	⊢ ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		nbgrssovtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	nbgrisvtx	⊢ ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑣 ∈ 𝑉 )
3		nbgrnself2	⊢ 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 )
4		df-nel	⊢ ( 𝑣 ∉ ( 𝐺 NeighbVtx 𝑋 ) ↔ ¬ 𝑣 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
5		neleq1	⊢ ( 𝑣 = 𝑋 → ( 𝑣 ∉ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) ) )
6	4 5	bitr3id	⊢ ( 𝑣 = 𝑋 → ( ¬ 𝑣 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) ) )
7	3 6	mpbiri	⊢ ( 𝑣 = 𝑋 → ¬ 𝑣 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
8	7	necon2ai	⊢ ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑣 ≠ 𝑋 )
9		eldifsn	⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑋 } ) ↔ ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑋 ) )
10	2 8 9	sylanbrc	⊢ ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑣 ∈ ( 𝑉 ∖ { 𝑋 } ) )
11	10	ssriv	⊢ ( 𝐺 NeighbVtx 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑋 } )