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 ⊢ V = Vtx ⁡ G
vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
Assertion vtxdusgrfvedg ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = e ∈ E | U ∈ e

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
2 vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
3 vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
6 1 4 5 3 vtxdusgrval ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i
7 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
8 uspgrushgr ⊢ G ∈ USHGraph → G ∈ USHGraph
9 7 8 syl ⊢ G ∈ USGraph → G ∈ USHGraph
10 1 2 vtxdushgrfvedglem ⊢ G ∈ USHGraph ∧ U ∈ V → i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i = e ∈ E | U ∈ e
11 9 10 sylan ⊢ G ∈ USGraph ∧ U ∈ V → i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i = e ∈ E | U ∈ e
12 6 11 eqtrd ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = e ∈ E | U ∈ e