Theorem nbgr0vtx

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

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

Proof

Step	Hyp	Ref	Expression
1		ral0	$$⊢\forall n\in \varnothing \neg \exists e\in \mathrm{Edg}\left(G\right)\left\{K,n\right\}\subseteq e$$
2		difeq1	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to \mathrm{Vtx}\left(G\right)\setminus \left\{K\right\}=\varnothing \setminus \left\{K\right\}$$
3		0dif	$$⊢\varnothing \setminus \left\{K\right\}=\varnothing$$
4	2 3	eqtrdi	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to \mathrm{Vtx}\left(G\right)\setminus \left\{K\right\}=\varnothing$$
5	4	raleqdv	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to \left(\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\leftrightarrow \forall n\in \varnothing \neg \exists e\in \mathrm{Edg}\left(G\right)\left\{K,n\right\}\subseteq e\right)$$
6	1 5	mpbiri	$$⊢\mathrm{Vtx}\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$$
7	6	nbgr0vtxlem	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to G\mathrm{NeighbVtx}K=\varnothing$$