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 𝑉 = ( Vtx ‘ 𝐺 )
vtxdg0e.i 𝐼 = ( iEdg ‘ 𝐺 )
vtxdgfisnn0.a 𝐴 = dom 𝐼
Assertion vtxdgfisnn0 ( ( 𝐴 ∈ Fin ∧ 𝑈𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 vtxdgf.v 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdg0e.i 𝐼 = ( iEdg ‘ 𝐺 )
3 vtxdgfisnn0.a 𝐴 = dom 𝐼
4 1 2 3 vtxdgfival ( ( 𝐴 ∈ Fin ∧ 𝑈𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) + ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) )
5 rabfi ( 𝐴 ∈ Fin → { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ∈ Fin )
6 hashcl ( { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ∈ Fin → ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) ∈ ℕ0 )
7 5 6 syl ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) ∈ ℕ0 )
8 rabfi ( 𝐴 ∈ Fin → { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ∈ Fin )
9 hashcl ( { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ∈ Fin → ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ∈ ℕ0 )
10 8 9 syl ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ∈ ℕ0 )
11 7 10 nn0addcld ( 𝐴 ∈ Fin → ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) + ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) ∈ ℕ0 )
12 11 adantr ( ( 𝐴 ∈ Fin ∧ 𝑈𝑉 ) → ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) + ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) ∈ ℕ0 )
13 4 12 eqeltrd ( ( 𝐴 ∈ Fin ∧ 𝑈𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℕ0 )