Metamath Proof Explorer

Theorem vtxdushgrfvedg

Description: The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020) (Proof shortened by AV, 5-May-2021)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
Assertion vtxdushgrfvedg ⊢ G ∈ USHGraph ∧ U ∈ V → D ⁡ U = e ∈ E | U ∈ e + 𝑒 e ∈ E | e = U

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
2 vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
3 vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
4 3 fveq1i ⊢ D ⁡ U = VtxDeg ⁡ G ⁡ U
5 4 a1i ⊢ G ∈ USHGraph ∧ U ∈ V → D ⁡ U = VtxDeg ⁡ G ⁡ U
6 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
7 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
8 1 6 7 vtxdgval ⊢ U ∈ V → VtxDeg ⁡ G ⁡ U = i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i + 𝑒 i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U
9 8 adantl ⊢ G ∈ USHGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i + 𝑒 i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U
10 1 2 vtxdushgrfvedglem ⊢ G ∈ USHGraph ∧ U ∈ V → i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i = e ∈ E | U ∈ e
11 fvex ⊢ iEdg ⁡ G ∈ V
12 11 dmex ⊢ dom ⁡ iEdg ⁡ G ∈ V
13 12 rabex ⊢ i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U ∈ V
14 13 a1i ⊢ G ∈ USHGraph ∧ U ∈ V → i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U ∈ V
15 eqid ⊢ i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U = i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U
16 eqeq1 ⊢ e = c → e = U ↔ c = U
17 16 cbvrabv ⊢ e ∈ E | e = U = c ∈ E | c = U
18 eqid ⊢ x ∈ i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U ⟼ iEdg ⁡ G ⁡ x = x ∈ i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U ⟼ iEdg ⁡ G ⁡ x
19 2 6 15 17 18 ushgredgedgloop ⊢ G ∈ USHGraph ∧ U ∈ V → x ∈ i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U ⟼ iEdg ⁡ G ⁡ x : i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U ⟶ 1-1 onto e ∈ E | e = U
20 14 19 hasheqf1od ⊢ G ∈ USHGraph ∧ U ∈ V → i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U = e ∈ E | e = U
21 10 20 oveq12d ⊢ G ∈ USHGraph ∧ U ∈ V → i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i + 𝑒 i ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ i = U = e ∈ E | U ∈ e + 𝑒 e ∈ E | e = U
22 5 9 21 3eqtrd ⊢ G ∈ USHGraph ∧ U ∈ V → D ⁡ U = e ∈ E | U ∈ e + 𝑒 e ∈ E | e = U