Theorem uspgrun

Description: The union U of two simple pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 16-Oct-2020)

	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 𝐹 ) = ∅ )
	uspgrun.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
	uspgrun.v	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
	uspgrun.un	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) )
Assertion	uspgrun	⊢ ( 𝜑 → 𝑈 ∈ 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		uspgrun.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
9		uspgrun.v	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
10		uspgrun.un	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) )
11		uspgrupgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
12	1 11	syl	⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
13		uspgrupgr	⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UPGraph )
14	2 13	syl	⊢ ( 𝜑 → 𝐻 ∈ UPGraph )
15	12 14 3 4 5 6 7 8 9 10	upgrun	⊢ ( 𝜑 → 𝑈 ∈ UPGraph )