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	$$⊢\mathrm{VtxDeg}=\left(g\in \mathrm{V}⟼⦋\mathrm{Vtx}\left(g\right)/v⦌⦋\mathrm{iEdg}\left(g\right)/e⦌\left(u\in v⟼\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvtxdg	$$class\mathrm{VtxDeg}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		cvtx	$$class\mathrm{Vtx}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class\mathrm{Vtx}\left(g\right)$$
6		vv	$$setvarv$$
7		ciedg	$$class\mathrm{iEdg}$$
8	4 7	cfv	$$class\mathrm{iEdg}\left(g\right)$$
9		ve	$$setvare$$
10		vu	$$setvaru$$
11	6	cv	$$setvarv$$
12		chash	$$class\left|.\right|$$
13		vx	$$setvarx$$
14	9	cv	$$setvare$$
15	14	cdm	$$class\mathrm{dom}e$$
16	10	cv	$$setvaru$$
17	13	cv	$$setvarx$$
18	17 14	cfv	$$classe\left(x\right)$$
19	16 18	wcel	$$wffu\in e\left(x\right)$$
20	19 13 15	crab	$$class\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}$$
21	20 12	cfv	$$class\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|$$
22		cxad	$$class{+}_{𝑒}$$
23	16	csn	$$class\left\{u\right\}$$
24	18 23	wceq	$$wffe\left(x\right)=\left\{u\right\}$$
25	24 13 15	crab	$$class\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}$$
26	25 12	cfv	$$class\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|$$
27	21 26 22	co	$$class\left(\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|\right)$$
28	10 11 27	cmpt	$$class\left(u\in v⟼\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|\right)$$
29	9 8 28	csb	$$class⦋\mathrm{iEdg}\left(g\right)/e⦌\left(u\in v⟼\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|\right)$$
30	6 5 29	csb	$$class⦋\mathrm{Vtx}\left(g\right)/v⦌⦋\mathrm{iEdg}\left(g\right)/e⦌\left(u\in v⟼\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|\right)$$
31	1 2 30	cmpt	$$class\left(g\in \mathrm{V}⟼⦋\mathrm{Vtx}\left(g\right)/v⦌⦋\mathrm{iEdg}\left(g\right)/e⦌\left(u\in v⟼\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|\right)\right)$$
32	0 31	wceq	$$wff\mathrm{VtxDeg}=\left(g\in \mathrm{V}⟼⦋\mathrm{Vtx}\left(g\right)/v⦌⦋\mathrm{iEdg}\left(g\right)/e⦌\left(u\in v⟼\left|\left\{x\in \mathrm{dom}e|u\in e\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in \mathrm{dom}e|e\left(x\right)=\left\{u\right\}\right\}\right|\right)\right)$$