Theorem umgrunop

Description: The union of two multigraphs (with the same vertex set): If <. V , E >. and <. V , F >. are multigraphs, then <. V , E u. F >. is a multigraph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		umgrun.g	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
2		umgrun.h	⊢ ( 𝜑 → 𝐻 ∈ UMGraph )
3		umgrun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
4		umgrun.f	⊢ 𝐹 = ( iEdg ‘ 𝐻 )
5		umgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
6		umgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
7		umgrun.i	⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
8		opex	⊢ ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ∈ V
9	8	a1i	⊢ ( 𝜑 → ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ∈ V )
10	5	fvexi	⊢ 𝑉 ∈ V
11	3	fvexi	⊢ 𝐸 ∈ V
12	4	fvexi	⊢ 𝐹 ∈ V
13	11 12	unex	⊢ ( 𝐸 ∪ 𝐹 ) ∈ V
14	10 13	pm3.2i	⊢ ( 𝑉 ∈ V ∧ ( 𝐸 ∪ 𝐹 ) ∈ V )
15		opvtxfv	⊢ ( ( 𝑉 ∈ V ∧ ( 𝐸 ∪ 𝐹 ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ) = 𝑉 )
16	14 15	mp1i	⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ) = 𝑉 )
17		opiedgfv	⊢ ( ( 𝑉 ∈ V ∧ ( 𝐸 ∪ 𝐹 ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ) = ( 𝐸 ∪ 𝐹 ) )
18	14 17	mp1i	⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ) = ( 𝐸 ∪ 𝐹 ) )
19	1 2 3 4 5 6 7 9 16 18	umgrun	⊢ ( 𝜑 → ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ∈ UMGraph )