Metamath Proof Explorer


Theorem vtxdgval

Description: The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 10-Dec-2020) (Revised by AV, 22-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 vtxdgval.v 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdgval.i 𝐼 = ( iEdg ‘ 𝐺 )
3 vtxdgval.a 𝐴 = dom 𝐼
4 1 1vgrex ( 𝑈𝑉𝐺 ∈ V )
5 1 2 3 vtxdgfval ( 𝐺 ∈ V → ( VtxDeg ‘ 𝐺 ) = ( 𝑢𝑉 ↦ ( ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) ) ) )
6 4 5 syl ( 𝑈𝑉 → ( VtxDeg ‘ 𝐺 ) = ( 𝑢𝑉 ↦ ( ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) ) ) )
7 6 fveq1d ( 𝑈𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( 𝑢𝑉 ↦ ( ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) ) ) ‘ 𝑈 ) )
8 eleq1 ( 𝑢 = 𝑈 → ( 𝑢 ∈ ( 𝐼𝑥 ) ↔ 𝑈 ∈ ( 𝐼𝑥 ) ) )
9 8 rabbidv ( 𝑢 = 𝑈 → { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } = { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } )
10 9 fveq2d ( 𝑢 = 𝑈 → ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) = ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) )
11 sneq ( 𝑢 = 𝑈 → { 𝑢 } = { 𝑈 } )
12 11 eqeq2d ( 𝑢 = 𝑈 → ( ( 𝐼𝑥 ) = { 𝑢 } ↔ ( 𝐼𝑥 ) = { 𝑈 } ) )
13 12 rabbidv ( 𝑢 = 𝑈 → { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } = { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } )
14 13 fveq2d ( 𝑢 = 𝑈 → ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) = ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) )
15 10 14 oveq12d ( 𝑢 = 𝑈 → ( ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) )
16 eqid ( 𝑢𝑉 ↦ ( ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) ) ) = ( 𝑢𝑉 ↦ ( ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) ) )
17 ovex ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) ∈ V
18 15 16 17 fvmpt ( 𝑈𝑉 → ( ( 𝑢𝑉 ↦ ( ( ♯ ‘ { 𝑥𝐴𝑢 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑢 } } ) ) ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) )
19 7 18 eqtrd ( 𝑈𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) )