This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ FinUSGraph → VtxDeg ⁡ G : V ⟶ ℕ 0

Proof

Step Hyp Ref Expression
1 vtxdgfusgrf.v ⊢ V = Vtx ⁡ G
2 fusgrfis ⊢ G ∈ FinUSGraph → Edg ⁡ G ∈ Fin
3 fusgrusgr ⊢ G ∈ FinUSGraph → G ∈ USGraph
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 eqid ⊢ Edg ⁡ G = Edg ⁡ G
6 4 5 usgredgffibi ⊢ G ∈ USGraph → Edg ⁡ G ∈ Fin ↔ iEdg ⁡ G ∈ Fin
7 3 6 syl ⊢ G ∈ FinUSGraph → Edg ⁡ G ∈ Fin ↔ iEdg ⁡ G ∈ Fin
8 usgrfun ⊢ G ∈ USGraph → Fun ⁡ iEdg ⁡ G
9 fundmfibi ⊢ Fun ⁡ iEdg ⁡ G → iEdg ⁡ G ∈ Fin ↔ dom ⁡ iEdg ⁡ G ∈ Fin
10 3 8 9 3syl ⊢ G ∈ FinUSGraph → iEdg ⁡ G ∈ Fin ↔ dom ⁡ iEdg ⁡ G ∈ Fin
11 7 10 bitrd ⊢ G ∈ FinUSGraph → Edg ⁡ G ∈ Fin ↔ dom ⁡ iEdg ⁡ G ∈ Fin
12 2 11 mpbid ⊢ G ∈ FinUSGraph → dom ⁡ iEdg ⁡ G ∈ Fin
13 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
14 1 4 13 vtxdgfisf ⊢ G ∈ FinUSGraph ∧ dom ⁡ iEdg ⁡ G ∈ Fin → VtxDeg ⁡ G : V ⟶ ℕ 0
15 12 14 mpdan ⊢ G ∈ FinUSGraph → VtxDeg ⁡ G : V ⟶ ℕ 0