Theorem vtxdusgradjvtx

Description: The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018) (Revised by AV, 23-Dec-2020)

	Ref	Expression
Hypotheses	vtxdusgradjvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdusgradjvtx.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	vtxdusgradjvtx	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdusgradjvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdusgradjvtx.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1	hashnbusgrvd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )
4	1 2	nbusgrvtx	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑈 ) = { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } )
5	4	fveq2d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) )
6	3 5	eqtr3d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) )