Metamath Proof Explorer

Theorem ushgrun

Description: The union U of two (undirected) simple hypergraphs G and H with the same vertex set V is a (not necessarily simple) hypergraph with the vertex set V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020) (Revised by AV, 24-Oct-2021)

Ref Expression
Hypotheses ushgrun.g ⊢ φ → G ∈ USHGraph
ushgrun.h ⊢ φ → H ∈ USHGraph
ushgrun.e ⊢ E = iEdg ⁡ G
ushgrun.f ⊢ F = iEdg ⁡ H
ushgrun.vg ⊢ V = Vtx ⁡ G
ushgrun.vh ⊢ φ → Vtx ⁡ H = V
ushgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
ushgrun.u ⊢ φ → U ∈ W
ushgrun.v ⊢ φ → Vtx ⁡ U = V
ushgrun.un ⊢ φ → iEdg ⁡ U = E ∪ F
Assertion ushgrun ⊢ φ → U ∈ UHGraph

Proof

Step Hyp Ref Expression
1 ushgrun.g ⊢ φ → G ∈ USHGraph
2 ushgrun.h ⊢ φ → H ∈ USHGraph
3 ushgrun.e ⊢ E = iEdg ⁡ G
4 ushgrun.f ⊢ F = iEdg ⁡ H
5 ushgrun.vg ⊢ V = Vtx ⁡ G
6 ushgrun.vh ⊢ φ → Vtx ⁡ H = V
7 ushgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
8 ushgrun.u ⊢ φ → U ∈ W
9 ushgrun.v ⊢ φ → Vtx ⁡ U = V
10 ushgrun.un ⊢ φ → iEdg ⁡ U = E ∪ F
11 ushgruhgr ⊢ G ∈ USHGraph → G ∈ UHGraph
12 1 11 syl ⊢ φ → G ∈ UHGraph
13 ushgruhgr ⊢ H ∈ USHGraph → H ∈ UHGraph
14 2 13 syl ⊢ φ → H ∈ UHGraph
15 12 14 3 4 5 6 7 8 9 10 uhgrun ⊢ φ → U ∈ UHGraph