Metamath Proof Explorer

Theorem vtxdgfusgrf

Description: The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		vtxdgfusgrf.v	$⊢ V = Vtx (G)$
2		fusgrfis	$⊢ G \in FinUSGraph \to Edg (G) \in Fin$
3		fusgrusgr	$⊢ G \in FinUSGraph \to G \in USGraph$
4		eqid	$⊢ iEdg (G) = iEdg (G)$
5		eqid	$⊢ Edg (G) = Edg (G)$
6	4 5	usgredgffibi	$⊢ G \in USGraph \to (Edg (G) \in Fin \leftrightarrow iEdg (G) \in Fin)$
7	3 6	syl	$⊢ G \in FinUSGraph \to (Edg (G) \in Fin \leftrightarrow iEdg (G) \in Fin)$
8		usgrfun	$⊢ G \in USGraph \to Fun iEdg (G)$
9		fundmfibi	$⊢ Fun iEdg (G) \to (iEdg (G) \in Fin \leftrightarrow dom iEdg (G) \in Fin)$
10	3 8 9	3syl	$⊢ G \in FinUSGraph \to (iEdg (G) \in Fin \leftrightarrow dom iEdg (G) \in Fin)$
11	7 10	bitrd	$⊢ G \in FinUSGraph \to (Edg (G) \in Fin \leftrightarrow dom iEdg (G) \in Fin)$
12	2 11	mpbid	$⊢ G \in FinUSGraph \to dom iEdg (G) \in Fin$
13		eqid	$⊢ dom iEdg (G) = dom iEdg (G)$
14	1 4 13	vtxdgfisf	$⊢ (G \in FinUSGraph \land dom iEdg (G) \in Fin) \to VtxDeg (G) : V ⟶ ℕ_{0}$
15	12 14	mpdan	$⊢ G \in FinUSGraph \to VtxDeg (G) : V ⟶ ℕ_{0}$