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 = ( Vtx ` G )
	vtxdlfgrval.i	|- I = ( iEdg ` G )
	vtxdlfgrval.a	|- A = dom I
	vtxdlfgrval.d	|- D = ( VtxDeg ` G )
Assertion	vtxdumgrval	|- ( ( G e. UMGraph /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdlfgrval.v	|- V = ( Vtx ` G )
2		vtxdlfgrval.i	|- I = ( iEdg ` G )
3		vtxdlfgrval.a	|- A = dom I
4		vtxdlfgrval.d	|- D = ( VtxDeg ` G )
5	1 2	umgrislfupgr	|- ( G e. UMGraph <-> ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
6	3	eqcomi	|- dom I = A
7	6	feq2i	|- ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> I : A --> { x e. ~P V | 2 <_ ( # ` x ) } )
8	7	biimpi	|- ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> I : A --> { x e. ~P V | 2 <_ ( # ` x ) } )
9	5 8	simplbiim	|- ( G e. UMGraph -> I : A --> { x e. ~P V | 2 <_ ( # ` x ) } )
10	1 2 3 4	vtxdlfgrval	|- ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )
11	9 10	sylan	|- ( ( G e. UMGraph /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )