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 ) |