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

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 ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) )