# Metamath Proof Explorer

## Theorem vtxdumgrval

Description: The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 23-Feb-2021)

Ref Expression
Hypotheses vtxdlfgrval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
vtxdlfgrval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
vtxdlfgrval.a ${⊢}{A}=\mathrm{dom}{I}$
vtxdlfgrval.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
Assertion vtxdumgrval ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {U}\in {V}\right)\to {D}\left({U}\right)=\left|\left\{{x}\in {A}|{U}\in {I}\left({x}\right)\right\}\right|$

### Proof

Step Hyp Ref Expression
1 vtxdlfgrval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 vtxdlfgrval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 vtxdlfgrval.a ${⊢}{A}=\mathrm{dom}{I}$
4 vtxdlfgrval.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
5 1 2 umgrislfupgr ${⊢}{G}\in \mathrm{UMGraph}↔\left({G}\in \mathrm{UPGraph}\wedge {I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\right)$
6 3 eqcomi ${⊢}\mathrm{dom}{I}={A}$
7 6 feq2i ${⊢}{I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}↔{I}:{A}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}$
8 7 biimpi ${⊢}{I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\to {I}:{A}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}$
9 5 8 simplbiim ${⊢}{G}\in \mathrm{UMGraph}\to {I}:{A}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}$
10 1 2 3 4 vtxdlfgrval ${⊢}\left({I}:{A}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\wedge {U}\in {V}\right)\to {D}\left({U}\right)=\left|\left\{{x}\in {A}|{U}\in {I}\left({x}\right)\right\}\right|$
11 9 10 sylan ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {U}\in {V}\right)\to {D}\left({U}\right)=\left|\left\{{x}\in {A}|{U}\in {I}\left({x}\right)\right\}\right|$