Metamath Proof Explorer

Theorem vtxdgfisnn0

Description: The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 11-Dec-2020) (Revised by AV, 22-Mar-2021)

		Ref	Expression
	Hypotheses	vtxdgf.v	$⊢ V = Vtx (G)$
		vtxdg0e.i	$⊢ I = iEdg (G)$
		vtxdgfisnn0.a	$⊢ A = dom I$
	Assertion	vtxdgfisnn0	$⊢ (A \in Fin \land U \in V) \to VtxDeg (G) (U) \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	$⊢ V = Vtx (G)$
2		vtxdg0e.i	$⊢ I = iEdg (G)$
3		vtxdgfisnn0.a	$⊢ A = dom I$
4	1 2 3	vtxdgfival	$⊢ (A \in Fin \land U \in V) \to VtxDeg (G) (U) = \|\{x \in A \| U \in I (x)\}\| + \|\{x \in A \| I (x) = \{U\}\}\|$
5		rabfi	$⊢ A \in Fin \to \{x \in A \| U \in I (x)\} \in Fin$
6		hashcl	$⊢ \{x \in A \| U \in I (x)\} \in Fin \to \|\{x \in A \| U \in I (x)\}\| \in ℕ_{0}$
7	5 6	syl	$⊢ A \in Fin \to \|\{x \in A \| U \in I (x)\}\| \in ℕ_{0}$
8		rabfi	$⊢ A \in Fin \to \{x \in A \| I (x) = \{U\}\} \in Fin$
9		hashcl	$⊢ \{x \in A \| I (x) = \{U\}\} \in Fin \to \|\{x \in A \| I (x) = \{U\}\}\| \in ℕ_{0}$
10	8 9	syl	$⊢ A \in Fin \to \|\{x \in A \| I (x) = \{U\}\}\| \in ℕ_{0}$
11	7 10	nn0addcld	$⊢ A \in Fin \to \|\{x \in A \| U \in I (x)\}\| + \|\{x \in A \| I (x) = \{U\}\}\| \in ℕ_{0}$
12	11	adantr	$⊢ (A \in Fin \land U \in V) \to \|\{x \in A \| U \in I (x)\}\| + \|\{x \in A \| I (x) = \{U\}\}\| \in ℕ_{0}$
13	4 12	eqeltrd	$⊢ (A \in Fin \land U \in V) \to VtxDeg (G) (U) \in ℕ_{0}$