Metamath Proof Explorer

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 ⊢φ→G∈UHGraph
uhgrun.h ⊢φ→H∈UHGraph
uhgrun.e ⊢E=iEdg⁡G
uhgrun.f ⊢F=iEdg⁡H
uhgrun.vg ⊢V=Vtx⁡G
uhgrun.vh ⊢φ→Vtx⁡H=V
uhgrun.i ⊢φ→dom⁡E∩dom⁡F=∅
Assertion uhgrunop ⊢φ→VE∪F∈UHGraph

Proof

Step Hyp Ref Expression
1 uhgrun.g ⊢φ→G∈UHGraph
2 uhgrun.h ⊢φ→H∈UHGraph
3 uhgrun.e ⊢E=iEdg⁡G
4 uhgrun.f ⊢F=iEdg⁡H
5 uhgrun.vg ⊢V=Vtx⁡G
6 uhgrun.vh ⊢φ→Vtx⁡H=V
7 uhgrun.i ⊢φ→dom⁡E∩dom⁡F=∅
8 opex ⊢VE∪F∈V
9 8 a1i ⊢φ→VE∪F∈V
10 5 fvexi ⊢V∈V
11 3 fvexi ⊢E∈V
12 4 fvexi ⊢F∈V
13 11 12 unex ⊢E∪F∈V
14 10 13 pm3.2i ⊢V∈V∧E∪F∈V
15 opvtxfv ⊢V∈V∧E∪F∈V→Vtx⁡VE∪F=V
16 14 15 mp1i ⊢φ→Vtx⁡VE∪F=V
17 opiedgfv ⊢V∈V∧E∪F∈V→iEdg⁡VE∪F=E∪F
18 14 17 mp1i ⊢φ→iEdg⁡VE∪F=E∪F
19 1 2 3 4 5 6 7 9 16 18 uhgrun ⊢φ→VE∪F∈UHGraph