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

Metamath Proof Explorer

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 𝑋 ) ⊆ ( 𝑉 ∖ { 𝑋 } )