Theorem clnbgr0vtx

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

	Ref	Expression
Assertion	clnbgr0vtx	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to GClNeighbVtxK=\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	clnbgrnvtx0	$$⊢K\notin \mathrm{Vtx}\left(G\right)\to GClNeighbVtxK=\varnothing$$
6	3 5	syl	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to GClNeighbVtxK=\varnothing$$