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 𝑋 ) = ∅ )