Metamath Proof Explorer

Theorem vtxdusgrfvedg

Description: The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢V=Vtx⁡G
vtxdushgrfvedg.e ⊢E=Edg⁡G
vtxdushgrfvedg.d ⊢D=VtxDeg⁡G
Assertion vtxdusgrfvedg ⊢G∈USGraph∧U∈V→D⁡U=e∈E|U∈e

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢V=Vtx⁡G
2 vtxdushgrfvedg.e ⊢E=Edg⁡G
3 vtxdushgrfvedg.d ⊢D=VtxDeg⁡G
4 eqid ⊢iEdg⁡G=iEdg⁡G
5 eqid ⊢dom⁡iEdg⁡G=dom⁡iEdg⁡G
6 1 4 5 3 vtxdusgrval ⊢G∈USGraph∧U∈V→D⁡U=i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i
7 usgruspgr ⊢G∈USGraph→G∈USHGraph
8 uspgrushgr ⊢G∈USHGraph→G∈USHGraph
9 7 8 syl ⊢G∈USGraph→G∈USHGraph
10 1 2 vtxdushgrfvedglem ⊢G∈USHGraph∧U∈V→i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i=e∈E|U∈e
11 9 10 sylan ⊢G∈USGraph∧U∈V→i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i=e∈E|U∈e
12 6 11 eqtrd ⊢G∈USGraph∧U∈V→D⁡U=e∈E|U∈e