Theorem vtxdusgrfvedg

Description: The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020)

	Ref	Expression
Hypotheses	vtxdushgrfvedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdushgrfvedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	vtxdushgrfvedg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	vtxdusgrfvedg	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdushgrfvedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdushgrfvedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		vtxdushgrfvedg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5		eqid	⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
6	1 4 5 3	vtxdusgrval	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) )
7		usgruspgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
8		uspgrushgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph )
9	7 8	syl	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USHGraph )
10	1 2	vtxdushgrfvedglem	⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )
11	9 10	sylan	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )
12	6 11	eqtrd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )