Theorem upgrunop

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

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

Proof

Step	Hyp	Ref	Expression
1		upgrun.g	⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
2		upgrun.h	⊢ ( 𝜑 → 𝐻 ∈ UPGraph )
3		upgrun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
4		upgrun.f	⊢ 𝐹 = ( iEdg ‘ 𝐻 )
5		upgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
6		upgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
7		upgrun.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	upgrun	⊢ ( 𝜑 → ⟨ 𝑉 , ( 𝐸 ∪ 𝐹 ) ⟩ ∈ UPGraph )