Metamath Proof Explorer

Theorem vtxduhgrun

Description: The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 21-Dec-2017) (Revised by AV, 12-Dec-2020) (Proof shortened by AV, 19-Feb-2021)

Ref Expression
Hypotheses vtxduhgrun.i ⊢ I = iEdg ⁡ G
vtxduhgrun.j ⊢ J = iEdg ⁡ H
vtxduhgrun.vg ⊢ V = Vtx ⁡ G
vtxduhgrun.vh ⊢ φ → Vtx ⁡ H = V
vtxduhgrun.vu ⊢ φ → Vtx ⁡ U = V
vtxduhgrun.d ⊢ φ → dom ⁡ I ∩ dom ⁡ J = ∅
vtxduhgrun.g ⊢ φ → G ∈ UHGraph
vtxduhgrun.h ⊢ φ → H ∈ UHGraph
vtxduhgrun.n ⊢ φ → N ∈ V
vtxduhgrun.u ⊢ φ → iEdg ⁡ U = I ∪ J
Assertion vtxduhgrun ⊢ φ → VtxDeg ⁡ U ⁡ N = VtxDeg ⁡ G ⁡ N + 𝑒 VtxDeg ⁡ H ⁡ N

Proof

Step Hyp Ref Expression
1 vtxduhgrun.i ⊢ I = iEdg ⁡ G
2 vtxduhgrun.j ⊢ J = iEdg ⁡ H
3 vtxduhgrun.vg ⊢ V = Vtx ⁡ G
4 vtxduhgrun.vh ⊢ φ → Vtx ⁡ H = V
5 vtxduhgrun.vu ⊢ φ → Vtx ⁡ U = V
6 vtxduhgrun.d ⊢ φ → dom ⁡ I ∩ dom ⁡ J = ∅
7 vtxduhgrun.g ⊢ φ → G ∈ UHGraph
8 vtxduhgrun.h ⊢ φ → H ∈ UHGraph
9 vtxduhgrun.n ⊢ φ → N ∈ V
10 vtxduhgrun.u ⊢ φ → iEdg ⁡ U = I ∪ J
11 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
12 7 11 syl ⊢ φ → Fun ⁡ I
13 2 uhgrfun ⊢ H ∈ UHGraph → Fun ⁡ J
14 8 13 syl ⊢ φ → Fun ⁡ J
15 1 2 3 4 5 6 12 14 9 10 vtxdun ⊢ φ → VtxDeg ⁡ U ⁡ N = VtxDeg ⁡ G ⁡ N + 𝑒 VtxDeg ⁡ H ⁡ N