Theorem nbgr0vtx

Description: In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020) (Proof shortened by AV, 10-May-2025)

	Ref	Expression
Assertion	nbgr0vtx	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to G\mathrm{NeighbVtx}K=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nel02	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to \neg K\in \mathrm{Vtx}\left(G\right)$$
2		df-nel	$$⊢K\notin \mathrm{Vtx}\left(G\right)\leftrightarrow \neg K\in \mathrm{Vtx}\left(G\right)$$
3	1 2	sylibr	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to K\notin \mathrm{Vtx}\left(G\right)$$
4		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
5	4	nbgrnvtx0	$$⊢K\notin \mathrm{Vtx}\left(G\right)\to G\mathrm{NeighbVtx}K=\varnothing$$
6	3 5	syl	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to G\mathrm{NeighbVtx}K=\varnothing$$