Theorem vtxdgval

Description: The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 10-Dec-2020) (Revised by AV, 22-Mar-2021)

	Ref	Expression
Hypotheses	vtxdgval.v	|- V = ( Vtx ` G )
	vtxdgval.i	|- I = ( iEdg ` G )
	vtxdgval.a	|- A = dom I
Assertion	vtxdgval	|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdgval.v	|- V = ( Vtx ` G )
2		vtxdgval.i	|- I = ( iEdg ` G )
3		vtxdgval.a	|- A = dom I
4	1	1vgrex	|- ( U e. V -> G e. _V )
5	1 2 3	vtxdgfval	|- ( G e. _V -> ( VtxDeg ` G ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )
6	4 5	syl	|- ( U e. V -> ( VtxDeg ` G ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )
7	6	fveq1d	|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) ` U ) )
8		eleq1	|- ( u = U -> ( u e. ( I ` x ) <-> U e. ( I ` x ) ) )
9	8	rabbidv	|- ( u = U -> { x e. A | u e. ( I ` x ) } = { x e. A | U e. ( I ` x ) } )
10	9	fveq2d	|- ( u = U -> ( # ` { x e. A | u e. ( I ` x ) } ) = ( # ` { x e. A | U e. ( I ` x ) } ) )
11		sneq	|- ( u = U -> { u } = { U } )
12	11	eqeq2d	|- ( u = U -> ( ( I ` x ) = { u } <-> ( I ` x ) = { U } ) )
13	12	rabbidv	|- ( u = U -> { x e. A | ( I ` x ) = { u } } = { x e. A | ( I ` x ) = { U } } )
14	13	fveq2d	|- ( u = U -> ( # ` { x e. A | ( I ` x ) = { u } } ) = ( # ` { x e. A | ( I ` x ) = { U } } ) )
15	10 14	oveq12d	|- ( u = U -> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
16		eqid	|- ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) )
17		ovex	|- ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) e. _V
18	15 16 17	fvmpt	|- ( U e. V -> ( ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
19	7 18	eqtrd	|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )