vtxduhgrfiun

Description: The degree of a vertex in the union of two hypergraphs of finite size 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-Jan-2018) (Revised by AV, 7-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	$⊢ φ \to Vtx (H) = V$
	vtxduhgrun.vu	$⊢ φ \to Vtx (U) = V$
	vtxduhgrun.d	$⊢ φ \to dom I \cap dom J = \emptyset$
	vtxduhgrun.g	$⊢ φ \to G \in UHGraph$
	vtxduhgrun.h	$⊢ φ \to H \in UHGraph$
	vtxduhgrun.n	$⊢ φ \to N \in V$
	vtxduhgrun.u	$⊢ φ \to iEdg (U) = I \cup J$
	vtxduhgrfiun.a	$⊢ φ \to dom I \in Fin$
	vtxduhgrfiun.b	$⊢ φ \to dom J \in Fin$
Assertion	vtxduhgrfiun	$⊢ φ \to 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	$⊢ φ \to Vtx (H) = V$
5		vtxduhgrun.vu	$⊢ φ \to Vtx (U) = V$
6		vtxduhgrun.d	$⊢ φ \to dom I \cap dom J = \emptyset$
7		vtxduhgrun.g	$⊢ φ \to G \in UHGraph$
8		vtxduhgrun.h	$⊢ φ \to H \in UHGraph$
9		vtxduhgrun.n	$⊢ φ \to N \in V$
10		vtxduhgrun.u	$⊢ φ \to iEdg (U) = I \cup J$
11		vtxduhgrfiun.a	$⊢ φ \to dom I \in Fin$
12		vtxduhgrfiun.b	$⊢ φ \to dom J \in Fin$
13	1	uhgrfun	$⊢ G \in UHGraph \to Fun I$
14	7 13	syl	$⊢ φ \to Fun I$
15	2	uhgrfun	$⊢ H \in UHGraph \to Fun J$
16	8 15	syl	$⊢ φ \to Fun J$
17	1 2 3 4 5 6 14 16 9 10 11 12	vtxdfiun	$⊢ φ \to VtxDeg (U) (N) = VtxDeg (G) (N) + VtxDeg (H) (N)$

Metamath Proof Explorer

Theorem vtxduhgrfiun

Proof