This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( 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 )