Metamath Proof Explorer

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 = Vtx ⁡ G
Assertion vtxdg0v ⊢ G = ∅ ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = 0

Proof

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