Metamath Proof Explorer

Theorem vtxdgfval

Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)

Ref Expression
Hypotheses vtxdgfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdgfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
vtxdgfval.a ⊢ 𝐴 = dom 𝐼
Assertion vtxdgfval ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) = ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )

Proof

Step Hyp Ref Expression
1 vtxdgfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdgfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 vtxdgfval.a ⊢ 𝐴 = dom 𝐼
4 df-vtxdg ⊢ VtxDeg = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
5 fvex ⊢ ( Vtx ‘ 𝑔 ) ∈ V
6 fvex ⊢ ( iEdg ‘ 𝑔 ) ∈ V
7 simpl ⊢ ( ( 𝑣 = ( Vtx ‘ 𝑔 ) ∧ 𝑒 = ( iEdg ‘ 𝑔 ) ) → 𝑣 = ( Vtx ‘ 𝑔 ) )
8 dmeq ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → dom 𝑒 = dom ( iEdg ‘ 𝑔 ) )
9 fveq1 ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( 𝑒 ‘ 𝑥 ) = ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) )
10 9 eleq2d ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) ↔ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) ) )
11 8 10 rabeqbidv ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } = { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } )
12 11 fveq2d ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) )
13 9 eqeq1d ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( ( 𝑒 ‘ 𝑥 ) = { 𝑢 } ↔ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } ) )
14 8 13 rabeqbidv ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } = { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } )
15 14 fveq2d ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) )
16 12 15 oveq12d ⊢ ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) = ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) ) )
17 16 adantl ⊢ ( ( 𝑣 = ( Vtx ‘ 𝑔 ) ∧ 𝑒 = ( iEdg ‘ 𝑔 ) ) → ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) = ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) ) )
18 7 17 mpteq12dv ⊢ ( ( 𝑣 = ( Vtx ‘ 𝑔 ) ∧ 𝑒 = ( iEdg ‘ 𝑔 ) ) → ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) = ( 𝑢 ∈ ( Vtx ‘ 𝑔 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
19 5 6 18 csbie2 ⊢ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) = ( 𝑢 ∈ ( Vtx ‘ 𝑔 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) ) )
20 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
21 20 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
22 fveq2 ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
23 22 dmeqd ⊢ ( 𝑔 = 𝐺 → dom ( iEdg ‘ 𝑔 ) = dom ( iEdg ‘ 𝐺 ) )
24 2 dmeqi ⊢ dom 𝐼 = dom ( iEdg ‘ 𝐺 )
25 3 24 eqtri ⊢ 𝐴 = dom ( iEdg ‘ 𝐺 )
26 23 25 eqtr4di ⊢ ( 𝑔 = 𝐺 → dom ( iEdg ‘ 𝑔 ) = 𝐴 )
27 22 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = 𝐼 )
28 27 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) )
29 28 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) ↔ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) ) )
30 26 29 rabeqbidv ⊢ ( 𝑔 = 𝐺 → { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } )
31 30 fveq2d ⊢ ( 𝑔 = 𝐺 → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) )
32 28 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } ↔ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } ) )
33 26 32 rabeqbidv ⊢ ( 𝑔 = 𝐺 → { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } = { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } )
34 33 fveq2d ⊢ ( 𝑔 = 𝐺 → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) = ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) )
35 31 34 oveq12d ⊢ ( 𝑔 = 𝐺 → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) )
36 21 35 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑢 ∈ ( Vtx ‘ 𝑔 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
37 36 adantl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺 ) → ( 𝑢 ∈ ( Vtx ‘ 𝑔 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝑔 ) ∣ ( ( iEdg ‘ 𝑔 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
38 19 37 syl5eq ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺 ) → ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑢 ∈ 𝑣 ↦ ( ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ ( 𝑒 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) = { 𝑢 } } ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
39 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
40 1 fvexi ⊢ 𝑉 ∈ V
41 mptexg ⊢ ( 𝑉 ∈ V → ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) ) ∈ V )
42 40 41 mp1i ⊢ ( 𝐺 ∈ 𝑊 → ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) ) ∈ V )
43 4 38 39 42 fvmptd2 ⊢ ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) = ( 𝑢 ∈ 𝑉 ↦ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑢 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑢 } } ) ) ) )