ushgrunop

Description: The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are simple hypergraphs, then <. V , E u. F >. is a (not necessarily simple) hypergraph - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020) (Revised by AV, 24-Oct-2021)

	Ref	Expression
Hypotheses	ushgrun.g	$⊢ φ \to G \in USHGraph$
	ushgrun.h	$⊢ φ \to H \in USHGraph$
	ushgrun.e	$⊢ E = iEdg (G)$
	ushgrun.f	$⊢ F = iEdg (H)$
	ushgrun.vg	$⊢ V = Vtx (G)$
	ushgrun.vh	$⊢ φ \to Vtx (H) = V$
	ushgrun.i	$⊢ φ \to dom E \cap dom F = \emptyset$
Assertion	ushgrunop	$⊢ φ \to ⟨V, E \cup F⟩ \in UHGraph$

Proof

Step	Hyp	Ref	Expression
1		ushgrun.g	$⊢ φ \to G \in USHGraph$
2		ushgrun.h	$⊢ φ \to H \in USHGraph$
3		ushgrun.e	$⊢ E = iEdg (G)$
4		ushgrun.f	$⊢ F = iEdg (H)$
5		ushgrun.vg	$⊢ V = Vtx (G)$
6		ushgrun.vh	$⊢ φ \to Vtx (H) = V$
7		ushgrun.i	$⊢ φ \to dom E \cap dom F = \emptyset$
8		ushgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
9	1 8	syl	$⊢ φ \to G \in UHGraph$
10		ushgruhgr	$⊢ H \in USHGraph \to H \in UHGraph$
11	2 10	syl	$⊢ φ \to H \in UHGraph$
12	9 11 3 4 5 6 7	uhgrunop	$⊢ φ \to ⟨V, E \cup F⟩ \in UHGraph$

Metamath Proof Explorer

Theorem ushgrunop

Proof