Theorem nbgr0edg

Description: In an empty graph (with no edges), every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020) (Proof shortened by AV, 15-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rzal	$$⊢\mathrm{Edg}\left(G\right)=\varnothing \to \forall e\in \mathrm{Edg}\left(G\right)\neg \left\{K,n\right\}\subseteq e$$
2		ralnex	$$⊢\forall e\in \mathrm{Edg}\left(G\right)\neg \left\{K,n\right\}\subseteq e\leftrightarrow \neg \exists e\in \mathrm{Edg}\left(G\right)\left\{K,n\right\}\subseteq e$$
3	1 2	sylib	$$⊢\mathrm{Edg}\left(G\right)=\varnothing \to \neg \exists e\in \mathrm{Edg}\left(G\right)\left\{K,n\right\}\subseteq e$$
4	3	ralrimivw	$$⊢\mathrm{Edg}\left(G\right)=\varnothing \to \forall n\in \left(\mathrm{Vtx}\left(G\right)\setminus \left\{K\right\}\right)\neg \exists e\in \mathrm{Edg}\left(G\right)\left\{K,n\right\}\subseteq e$$
5	4	nbgr0vtxlem	$$⊢\mathrm{Edg}\left(G\right)=\varnothing \to G\mathrm{NeighbVtx}K=\varnothing$$