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 ⊢ φ → V E ∪ 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 ⊢ V E ∪ F ∈ V
9 8 a1i ⊢ φ → V E ∪ 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 ⁡ V E ∪ F = V
16 14 15 mp1i ⊢ φ → Vtx ⁡ V E ∪ F = V
17 opiedgfv ⊢ V ∈ V ∧ E ∪ F ∈ V → iEdg ⁡ V E ∪ F = E ∪ F
18 14 17 mp1i ⊢ φ → iEdg ⁡ V E ∪ F = E ∪ F
19 1 2 3 4 5 6 7 9 16 18 uhgrun ⊢ φ → V E ∪ F ∈ UHGraph