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