Theorem usgrunop

Description: The union of two simple graphs (with the same vertex set): If <. V , E >. and <. V , F >. are simple graphs, then <. V , E u. F >. is a multigraph (not necessarily a simple graph!) - 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)

	Ref	Expression
Hypotheses	usgrun.g	⊢ ( 𝜑 → 𝐺 ∈ USGraph )
	usgrun.h	⊢ ( 𝜑 → 𝐻 ∈ USGraph )
	usgrun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	usgrun.f	⊢ 𝐹 = ( iEdg ‘ 𝐻 )
	usgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	usgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
	usgrun.i	⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
Assertion	usgrunop	⊢ ( 𝜑 → ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ∈ UMGraph )

Proof

Step	Hyp	Ref	Expression
1		usgrun.g	⊢ ( 𝜑 → 𝐺 ∈ USGraph )
2		usgrun.h	⊢ ( 𝜑 → 𝐻 ∈ USGraph )
3		usgrun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
4		usgrun.f	⊢ 𝐹 = ( iEdg ‘ 𝐻 )
5		usgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
6		usgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
7		usgrun.i	⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
8		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
9	1 8	syl	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
10		usgrumgr	⊢ ( 𝐻 ∈ USGraph → 𝐻 ∈ UMGraph )
11	2 10	syl	⊢ ( 𝜑 → 𝐻 ∈ UMGraph )
12	9 11 3 4 5 6 7	umgrunop	⊢ ( 𝜑 → ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ∈ UMGraph )