Theorem vtxdg0e

Description: The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph (see also the induction steps vdegp1ai , vdegp1bi and vdegp1ci ). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020) (Revised by AV, 22-Mar-2021)

	Ref	Expression
Hypotheses	vtxdgf.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdg0e.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	vtxdg0e	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdg0e.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3	2	eqeq1i	⊢ ( 𝐼 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ )
4		dmeq	⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → dom ( iEdg ‘ 𝐺 ) = dom ∅ )
5		dm0	⊢ dom ∅ = ∅
6	4 5	eqtrdi	⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → dom ( iEdg ‘ 𝐺 ) = ∅ )
7		0fin	⊢ ∅ ∈ Fin
8	6 7	eqeltrdi	⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → dom ( iEdg ‘ 𝐺 ) ∈ Fin )
9	3 8	sylbi	⊢ ( 𝐼 = ∅ → dom ( iEdg ‘ 𝐺 ) ∈ Fin )
10		simpl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐼 = ∅ ) → 𝑈 ∈ 𝑉 )
11		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
12		eqid	⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
13	1 11 12	vtxdgfival	⊢ ( ( dom ( iEdg ‘ 𝐺 ) ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) ) )
14	9 10 13	syl2an2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) ) )
15	3 6	sylbi	⊢ ( 𝐼 = ∅ → dom ( iEdg ‘ 𝐺 ) = ∅ )
16	15	adantl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐼 = ∅ ) → dom ( iEdg ‘ 𝐺 ) = ∅ )
17		rabeq	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑥 ∈ ∅ ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } )
18		rab0	⊢ { 𝑥 ∈ ∅ ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅
19	17 18	eqtrdi	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅ )
20	19	fveq2d	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = ( ♯ ‘ ∅ ) )
21		hash0	⊢ ( ♯ ‘ ∅ ) = 0
22	20 21	eqtrdi	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 0 )
23		rabeq	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } = { 𝑥 ∈ ∅ ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } )
24	23	fveq2d	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) = ( ♯ ‘ { 𝑥 ∈ ∅ ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) )
25		rab0	⊢ { 𝑥 ∈ ∅ ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } = ∅
26	25	fveq2i	⊢ ( ♯ ‘ { 𝑥 ∈ ∅ ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) = ( ♯ ‘ ∅ )
27	26 21	eqtri	⊢ ( ♯ ‘ { 𝑥 ∈ ∅ ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) = 0
28	24 27	eqtrdi	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) = 0 )
29	22 28	oveq12d	⊢ ( dom ( iEdg ‘ 𝐺 ) = ∅ → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) ) = ( 0 + 0 ) )
30	16 29	syl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) ) = ( 0 + 0 ) )
31		00id	⊢ ( 0 + 0 ) = 0
32	30 31	eqtrdi	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑈 } } ) ) = 0 )
33	14 32	eqtrd	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )