Metamath Proof Explorer

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 )