Metamath Proof Explorer

Theorem vtxdgf

Description: The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 10-Dec-2020)

		Ref	Expression
	Hypothesis	vtxdgf.v	$⊢ V = Vtx (G)$
	Assertion	vtxdgf	$⊢ G \in W \to VtxDeg (G) : V ⟶ ℕ_{0}^{*}$

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	$⊢ V = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3		eqid	$⊢ dom iEdg (G) = dom iEdg (G)$
4	1 2 3	vtxdgfval	$⊢ G \in W \to VtxDeg (G) = (u \in V ⟼ \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\|)$
5		eqid	$⊢ \{x \in dom iEdg (G) \| u \in iEdg (G) (x)\} = \{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}$
6		fvex	$⊢ iEdg (G) \in V$
7		dmexg	$⊢ iEdg (G) \in V \to dom iEdg (G) \in V$
8	6 7	mp1i	$⊢ (G \in W \land u \in V) \to dom iEdg (G) \in V$
9	5 8	rabexd	$⊢ (G \in W \land u \in V) \to \{x \in dom iEdg (G) \| u \in iEdg (G) (x)\} \in V$
10		hashxnn0	$⊢ \{x \in dom iEdg (G) \| u \in iEdg (G) (x)\} \in V \to \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| \in ℕ_{0}^{*}$
11	9 10	syl	$⊢ (G \in W \land u \in V) \to \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| \in ℕ_{0}^{*}$
12		eqid	$⊢ \{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\} = \{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}$
13	12 8	rabexd	$⊢ (G \in W \land u \in V) \to \{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\} \in V$
14		hashxnn0	$⊢ \{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\} \in V \to \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\| \in ℕ_{0}^{*}$
15	13 14	syl	$⊢ (G \in W \land u \in V) \to \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\| \in ℕ_{0}^{*}$
16		xnn0xaddcl	$⊢ (\|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| \in ℕ_{0}^{} \land \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\| \in ℕ_{0}^{}) \to \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\| \in ℕ_{0}^{*}$
17	11 15 16	syl2anc	$⊢ (G \in W \land u \in V) \to \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\| \in ℕ_{0}^{*}$
18	4 17	fmpt3d	$⊢ G \in W \to VtxDeg (G) : V ⟶ ℕ_{0}^{*}$