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=\mathrm{Vtx}\left(G\right)$$
	vtxdgval.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	vtxdgval.a	$$⊢A=\mathrm{dom}I$$
Assertion	vtxdgval	$$⊢U\in V\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}\right|$$

Proof

Step	Hyp	Ref	Expression
1		vtxdgval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		vtxdgval.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		vtxdgval.a	$$⊢A=\mathrm{dom}I$$
4	1	1vgrex	$$⊢U\in V\to G\in \mathrm{V}$$
5	1 2 3	vtxdgfval	$$⊢G\in \mathrm{V}\to \mathrm{VtxDeg}\left(G\right)=\left(u\in V⟼\left|\left\{x\in A|u\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|\right)$$
6	4 5	syl	$$⊢U\in V\to \mathrm{VtxDeg}\left(G\right)=\left(u\in V⟼\left|\left\{x\in A|u\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|\right)$$
7	6	fveq1d	$$⊢U\in V\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=\left(u\in V⟼\left|\left\{x\in A|u\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|\right)\left(U\right)$$
8		eleq1	$$⊢u=U\to \left(u\in I\left(x\right)\leftrightarrow U\in I\left(x\right)\right)$$
9	8	rabbidv	$$⊢u=U\to \left\{x\in A|u\in I\left(x\right)\right\}=\left\{x\in A|U\in I\left(x\right)\right\}$$
10	9	fveq2d	$$⊢u=U\to \left|\left\{x\in A|u\in I\left(x\right)\right\}\right|=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|$$
11		sneq	$$⊢u=U\to \left\{u\right\}=\left\{U\right\}$$
12	11	eqeq2d	$$⊢u=U\to \left(I\left(x\right)=\left\{u\right\}\leftrightarrow I\left(x\right)=\left\{U\right\}\right)$$
13	12	rabbidv	$$⊢u=U\to \left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}=\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}$$
14	13	fveq2d	$$⊢u=U\to \left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|=\left|\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}\right|$$
15	10 14	oveq12d	$$⊢u=U\to \left|\left\{x\in A|u\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}\right|$$
16		eqid	$$⊢\left(u\in V⟼\left|\left\{x\in A|u\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|\right)=\left(u\in V⟼\left|\left\{x\in A|u\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|\right)$$
17		ovex	$$⊢\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}\right|\in \mathrm{V}$$
18	15 16 17	fvmpt	$$⊢U\in V\to \left(u\in V⟼\left|\left\{x\in A|u\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{u\right\}\right\}\right|\right)\left(U\right)=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}\right|$$
19	7 18	eqtrd	$$⊢U\in V\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|{+}_{𝑒}\left|\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}\right|$$