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

Metamath Proof Explorer

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 ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )