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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vtxdgfusgrf ( 𝐺 ∈ FinUSGraph → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 )

Proof

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