Definition df-vtxdg 16093

Description: Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain 𝑢 "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 infinite), the extended addition +_𝑒 is used for the summation of the number of "ordinary" edges" and the number of "loops".

Because we cannot in general show that an arbitrary set is either finite or infinite (see inffiexmid 7091), this definition is not as general as it may appear. But we keep it for consistency with the Metamath Proof Explorer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)

Assertion

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

Distinct variable group:   𝑒,𝑔,𝑢,𝑣,𝑥

Detailed syntax breakdown of Definition df-vtxdg

Step	Hyp	Ref	Expression
1		cvtxdg 16092	. 2 class VtxDeg
2		vg	. . 3 setvar 𝑔
3		cvv 2800	. . 3 class V
4		vv	. . . 4 setvar 𝑣
5	2	cv 1394	. . . . 5 class 𝑔
6		cvtx 15853	. . . . 5 class Vtx
7	5, 6	cfv 5324	. . . 4 class (Vtx‘𝑔)
8		ve	. . . . 5 setvar 𝑒
9		ciedg 15854	. . . . . 6 class iEdg
10	5, 9	cfv 5324	. . . . 5 class (iEdg‘𝑔)
11		vu	. . . . . 6 setvar 𝑢
12	4	cv 1394	. . . . . 6 class 𝑣
13	11	cv 1394	. . . . . . . . . 10 class 𝑢
14		vx	. . . . . . . . . . . 12 setvar 𝑥
15	14	cv 1394	. . . . . . . . . . 11 class 𝑥
16	8	cv 1394	. . . . . . . . . . 11 class 𝑒
17	15, 16	cfv 5324	. . . . . . . . . 10 class (𝑒‘𝑥)
18	13, 17	wcel 2200	. . . . . . . . 9 wff 𝑢 ∈ (𝑒‘𝑥)
19	16	cdm 4723	. . . . . . . . 9 class dom 𝑒
20	18, 14, 19	crab 2512	. . . . . . . 8 class {𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}
21		chash 11027	. . . . . . . 8 class ♯
22	20, 21	cfv 5324	. . . . . . 7 class (♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)})
23	13	csn 3667	. . . . . . . . . 10 class {𝑢}
24	17, 23	wceq 1395	. . . . . . . . 9 wff (𝑒‘𝑥) = {𝑢}
25	24, 14, 19	crab 2512	. . . . . . . 8 class {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}
26	25, 21	cfv 5324	. . . . . . 7 class (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})
27		cxad 9995	. . . . . . 7 class +𝑒
28	22, 26, 27	co 6013	. . . . . 6 class ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))
29	11, 12, 28	cmpt 4148	. . . . 5 class (𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))
30	8, 10, 29	csb 3125	. . . 4 class ⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))
31	4, 7, 30	csb 3125	. . 3 class ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))
32	2, 3, 31	cmpt 4148	. 2 class (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))
33	1, 32	wceq 1395	1 wff VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))

This definition is referenced by:  vtxdgfval  16094