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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	vtxdg0v	⊢ ( ( 𝐺 = ∅ ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	eleq2i	⊢ ( 𝑈 ∈ 𝑉 ↔ 𝑈 ∈ ( Vtx ‘ 𝐺 ) )
3		fveq2	⊢ ( 𝐺 = ∅ → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ∅ ) )
4		vtxval0	⊢ ( Vtx ‘ ∅ ) = ∅
5	3 4	eqtrdi	⊢ ( 𝐺 = ∅ → ( Vtx ‘ 𝐺 ) = ∅ )
6	5	eleq2d	⊢ ( 𝐺 = ∅ → ( 𝑈 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝑈 ∈ ∅ ) )
7	2 6	bitrid	⊢ ( 𝐺 = ∅ → ( 𝑈 ∈ 𝑉 ↔ 𝑈 ∈ ∅ ) )
8		noel	⊢ ¬ 𝑈 ∈ ∅
9	8	pm2.21i	⊢ ( 𝑈 ∈ ∅ → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )
10	7 9	biimtrdi	⊢ ( 𝐺 = ∅ → ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 ) )
11	10	imp	⊢ ( ( 𝐺 = ∅ ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )