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 e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { e e. E | U e. 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 e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) )
7		usgruspgr	|- ( G e. USGraph -> G e. USPGraph )
8		uspgrushgr	|- ( G e. USPGraph -> G e. USHGraph )
9	7 8	syl	|- ( G e. USGraph -> G e. USHGraph )
10	1 2	vtxdushgrfvedglem	|- ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) )
11	9 10	sylan	|- ( ( G e. USGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) )
12	6 11	eqtrd	|- ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { e e. E | U e. e } ) )