Theorem vtxdushgrfvedg

Description: The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020) (Proof shortened by AV, 5-May-2021)

	Ref	Expression
Hypotheses	vtxdushgrfvedg.v	|- V = ( Vtx ` G )
	vtxdushgrfvedg.e	|- E = ( Edg ` G )
	vtxdushgrfvedg.d	|- D = ( VtxDeg ` G )
Assertion	vtxdushgrfvedg	|- ( ( G e. USHGraph /\ U e. V ) -> ( D ` U ) = ( ( # ` { e e. E | U e. e } ) +e ( # ` { e e. E | e = { U } } ) ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdushgrfvedg.v	|- V = ( Vtx ` G )
2		vtxdushgrfvedg.e	|- E = ( Edg ` G )
3		vtxdushgrfvedg.d	|- D = ( VtxDeg ` G )
4	3	fveq1i	|- ( D ` U ) = ( ( VtxDeg ` G ) ` U )
5	4	a1i	|- ( ( G e. USHGraph /\ U e. V ) -> ( D ` U ) = ( ( VtxDeg ` G ) ` U ) )
6		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
7		eqid	|- dom ( iEdg ` G ) = dom ( iEdg ` G )
8	1 6 7	vtxdgval	|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) ) )
9	8	adantl	|- ( ( G e. USHGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) ) )
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		fvex	|- ( iEdg ` G ) e. _V
12	11	dmex	|- dom ( iEdg ` G ) e. _V
13	12	rabex	|- { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } e. _V
14	13	a1i	|- ( ( G e. USHGraph /\ U e. V ) -> { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } e. _V )
15		eqid	|- { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } = { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } }
16		eqeq1	|- ( e = c -> ( e = { U } <-> c = { U } ) )
17	16	cbvrabv	|- { e e. E | e = { U } } = { c e. E | c = { U } }
18		eqid	|- ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } |-> ( ( iEdg ` G ) ` x ) ) = ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } |-> ( ( iEdg ` G ) ` x ) )
19	2 6 15 17 18	ushgredgedgloop	|- ( ( G e. USHGraph /\ U e. V ) -> ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } |-> ( ( iEdg ` G ) ` x ) ) : { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } -1-1-onto-> { e e. E | e = { U } } )
20	14 19	hasheqf1od	|- ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) = ( # ` { e e. E | e = { U } } ) )
21	10 20	oveq12d	|- ( ( G e. USHGraph /\ U e. V ) -> ( ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) ) = ( ( # ` { e e. E | U e. e } ) +e ( # ` { e e. E | e = { U } } ) ) )
22	5 9 21	3eqtrd	|- ( ( G e. USHGraph /\ U e. V ) -> ( D ` U ) = ( ( # ` { e e. E | U e. e } ) +e ( # ` { e e. E | e = { U } } ) ) )