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