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

Metamath Proof Explorer

Theorem nbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has no neighbors in G . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Hypothesis nbgrel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion nbgrnvtx0 ( 𝑋 ∉ 𝑉 → ( 𝐺 NeighbVtx 𝑋 ) = ∅ )

Proof

Step Hyp Ref Expression
1 nbgrel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 csbfv ⊢ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 )
3 1 2 eqtr4i ⊢ 𝑉 = ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 )
4 neleq2 ⊢ ( 𝑉 = ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) → ( 𝑋 ∉ 𝑉 ↔ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ) )
5 3 4 ax-mp ⊢ ( 𝑋 ∉ 𝑉 ↔ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) )
6 5 biimpi ⊢ ( 𝑋 ∉ 𝑉 → 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) )
7 6 olcd ⊢ ( 𝑋 ∉ 𝑉 → ( 𝐺 ∉ V ∨ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ) )
8 df-nbgr ⊢ NeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
9 8 mpoxneldm ⊢ ( ( 𝐺 ∉ V ∨ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ) → ( 𝐺 NeighbVtx 𝑋 ) = ∅ )
10 7 9 syl ⊢ ( 𝑋 ∉ 𝑉 → ( 𝐺 NeighbVtx 𝑋 ) = ∅ )