Definition df-vtxdg

Description: Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain u "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +e is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)

	Ref	Expression
Assertion	df-vtxdg	⊢ VtxDeg = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvtxdg	⊢ VtxDeg
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		cvtx	⊢ Vtx
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( Vtx ‘ 𝑔 )
6		vv	⊢ 𝑣
7		ciedg	⊢ iEdg
8	4 7	cfv	⊢ ( iEdg ‘ 𝑔 )
9		ve	⊢ 𝑒
10		vu	⊢ 𝑢
11	6	cv	⊢ 𝑣
12		chash	⊢ ♯
13		vx	⊢ 𝑥
14	9	cv	⊢ 𝑒
15	14	cdm	⊢ dom 𝑒
16	10	cv	⊢ 𝑢
17	13	cv	⊢ 𝑥
18	17 14	cfv	⊢ ( 𝑒 ‘ 𝑥 )
19	16 18	wcel	⊢ 𝑢 ∈ ( 𝑒 ‘ 𝑥 )
20	19 13 15	crab	⊢ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) }
21	20 12	cfv	⊢ ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } )
22		cxad	⊢ +𝑒
23	16	csn	⊢ { 𝑢 }
24	18 23	wceq	⊢ ( 𝑒 ‘ 𝑥 ) = { 𝑢 }
25	24 13 15	crab	⊢ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } }
26	25 12	cfv	⊢ ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } )
27	21 26 22	co	⊢ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) )
28	10 11 27	cmpt	⊢ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) )
29	9 8 28	csb	⊢ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) )
30	6 5 29	csb	⊢ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) )
31	1 2 30	cmpt	⊢ ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
32	0 31	wceq	⊢ VtxDeg = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )