Metamath Proof Explorer

Theorem vdumgr0

Description: A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypothesis vdumgr0.v ⊢V=Vtx⁡G
Assertion vdumgr0 ⊢G∈UMGraph∧N∈V∧V=1→VtxDeg⁡G⁡N=0

Proof

Step Hyp Ref Expression
1 vdumgr0.v ⊢V=Vtx⁡G
2 umgruhgr ⊢G∈UMGraph→G∈UHGraph
3 2 3ad2ant1 ⊢G∈UMGraph∧N∈V∧V=1→G∈UHGraph
4 simp3 ⊢G∈UMGraph∧N∈V∧V=1→V=1
5 eqid ⊢iEdg⁡G=iEdg⁡G
6 1 5 umgrislfupgr ⊢G∈UMGraph↔G∈UPGraph∧iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫V|2≤x
7 6 simprbi ⊢G∈UMGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫V|2≤x
8 7 3ad2ant1 ⊢G∈UMGraph∧N∈V∧V=1→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫V|2≤x
9 3 4 8 3jca ⊢G∈UMGraph∧N∈V∧V=1→G∈UHGraph∧V=1∧iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫V|2≤x
10 simp2 ⊢G∈UMGraph∧N∈V∧V=1→N∈V
11 eqid ⊢x∈𝒫V|2≤x=x∈𝒫V|2≤x
12 1 5 11 vtxdlfuhgr1v ⊢G∈UHGraph∧V=1∧iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫V|2≤x→N∈V→VtxDeg⁡G⁡N=0
13 9 10 12 sylc ⊢G∈UMGraph∧N∈V∧V=1→VtxDeg⁡G⁡N=0