Theorem usgrun

Description: The union U of two simple graphs G and H with the same vertex set V is a multigraph (not necessarily a simple graph!) with the vertex V and the union ( E u. F ) of the (indexed) edges. (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 𝐹 ) = ∅ )
	usgrun.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
	usgrun.v	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
	usgrun.un	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) )
Assertion	usgrun	⊢ ( 𝜑 → 𝑈 ∈ 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		usgrun.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
9		usgrun.v	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
10		usgrun.un	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) )
11		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
12	1 11	syl	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
13		usgrumgr	⊢ ( 𝐻 ∈ USGraph → 𝐻 ∈ UMGraph )
14	2 13	syl	⊢ ( 𝜑 → 𝐻 ∈ UMGraph )
15	12 14 3 4 5 6 7 8 9 10	umgrun	⊢ ( 𝜑 → 𝑈 ∈ UMGraph )