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

Metamath Proof Explorer

Definition df-vtxdg

Description: Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain u "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +e is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)

Ref Expression
Assertion df-vtxdg VtxDeg = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvtxdg ⊢ VtxDeg
1 vg ⊢ 𝑔
2 cvv ⊢ V
3 cvtx ⊢ Vtx
4 1 cv ⊢ 𝑔
5 4 3 cfv ⊢ ( Vtx ‘ 𝑔 )
6 vv ⊢ 𝑣
7 ciedg ⊢ iEdg
8 4 7 cfv ⊢ ( iEdg ‘ 𝑔 )
9 ve ⊢ 𝑒
10 vu ⊢ 𝑢
11 6 cv ⊢ 𝑣
12 chash ⊢ ♯
13 vx ⊢ 𝑥
14 9 cv ⊢ 𝑒
15 14 cdm ⊢ dom 𝑒
16 10 cv ⊢ 𝑢
17 13 cv ⊢ 𝑥
18 17 14 cfv ⊢ ( 𝑒 ‘ 𝑥 )
19 16 18 wcel ⊢ 𝑢 ∈ ( 𝑒 ‘ 𝑥 )
20 19 13 15 crab ⊢ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) }
21 20 12 cfv ⊢ ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } )
22 cxad ⊢ +𝑒
23 16 csn ⊢ { 𝑢 }
24 18 23 wceq ⊢ ( 𝑒 ‘ 𝑥 ) = { 𝑢 }
25 24 13 15 crab ⊢ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } }
26 25 12 cfv ⊢ ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } )
27 21 26 22 co ⊢ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) )
28 10 11 27 cmpt ⊢ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) )
29 9 8 28 csb ⊢ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) )
30 6 5 29 csb ⊢ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) )
31 1 2 30 cmpt ⊢ ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
32 0 31 wceq ⊢ VtxDeg = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )