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

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 )