Theorem uhgrunop

Description: The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are hypergraphs, then <. V , E u. F >. is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 11-Oct-2020) (Revised by AV, 24-Oct-2021)

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

Proof

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