Theorem vtxdg0v

Description: The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020)

	Ref	Expression
Hypothesis	vtxdgf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	vtxdg0v	$$⊢\left(G=\varnothing \wedge U\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	eleq2i	$$⊢U\in V\leftrightarrow U\in \mathrm{Vtx}\left(G\right)$$
3		fveq2	$$⊢G=\varnothing \to \mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(\varnothing \right)$$
4		vtxval0	$$⊢\mathrm{Vtx}\left(\varnothing \right)=\varnothing$$
5	3 4	eqtrdi	$$⊢G=\varnothing \to \mathrm{Vtx}\left(G\right)=\varnothing$$
6	5	eleq2d	$$⊢G=\varnothing \to \left(U\in \mathrm{Vtx}\left(G\right)\leftrightarrow U\in \varnothing \right)$$
7	2 6	bitrid	$$⊢G=\varnothing \to \left(U\in V\leftrightarrow U\in \varnothing \right)$$
8		noel	$$⊢\neg U\in \varnothing$$
9	8	pm2.21i	$$⊢U\in \varnothing \to \mathrm{VtxDeg}\left(G\right)\left(U\right)=0$$
10	7 9	syl6bi	$$⊢G=\varnothing \to \left(U\in V\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=0\right)$$
11	10	imp	$$⊢\left(G=\varnothing \wedge U\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=0$$