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

Metamath Proof Explorer

Theorem vtxdgf

Description: The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 10-Dec-2020)

Ref Expression
Hypothesis vtxdgf.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vtxdgf ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0* )

Proof

Step Hyp Ref Expression
1 vtxdgf.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 eqid ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
4 1 2 3 vtxdgfval ⊢ ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) = ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
5 eqid ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) }
6 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
7 dmexg ⊢ ( ( iEdg ‘ 𝐺 ) ∈ V → dom ( iEdg ‘ 𝐺 ) ∈ V )
8 6 7 mp1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑢 ∈ 𝑉 ) → dom ( iEdg ‘ 𝐺 ) ∈ V )
9 5 8 rabexd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑢 ∈ 𝑉 ) → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V )
10 hashxnn0 ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ ℕ0* )
11 9 10 syl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑢 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ ℕ0* )
12 eqid ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } }
13 12 8 rabexd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑢 ∈ 𝑉 ) → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ∈ V )
14 hashxnn0 ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ∈ V → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ∈ ℕ0* )
15 13 14 syl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑢 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ∈ ℕ0* )
16 xnn0xaddcl ⊢ ( ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ ℕ0* ∧ ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ∈ ℕ0* ) → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ∈ ℕ0* )
17 11 15 16 syl2anc ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑢 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ∈ ℕ0* )
18 4 17 fmpt3d ⊢ ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0* )