Theorem uspgrunop

Description: The union of two simple pseudographs (with the same vertex set): If <. V , E >. and <. V , F >. are simple pseudographs, then <. V , E u. F >. is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Revised by AV, 24-Oct-2021)

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

Proof

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