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 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 | ⊢ ( 𝜑 → 𝐺 ∈ USHGraph ) | |
| ushgrun.h | ⊢ ( 𝜑 → 𝐻 ∈ USHGraph ) | ||
| ushgrun.e | ⊢ 𝐸 = ( iEdg ‘ 𝐺 ) | ||
| ushgrun.f | ⊢ 𝐹 = ( iEdg ‘ 𝐻 ) | ||
| ushgrun.vg | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | ||
| ushgrun.vh | ⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 ) | ||
| ushgrun.i | ⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ ) | ||
| ushgrun.u | ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 ) | ||
| ushgrun.v | ⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 ) | ||
| ushgrun.un | ⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) ) | ||
| Assertion | ushgrun | ⊢ ( 𝜑 → 𝑈 ∈ UHGraph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ushgrun.g | ⊢ ( 𝜑 → 𝐺 ∈ USHGraph ) | |
| 2 | ushgrun.h | ⊢ ( 𝜑 → 𝐻 ∈ USHGraph ) | |
| 3 | ushgrun.e | ⊢ 𝐸 = ( iEdg ‘ 𝐺 ) | |
| 4 | ushgrun.f | ⊢ 𝐹 = ( iEdg ‘ 𝐻 ) | |
| 5 | ushgrun.vg | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 6 | ushgrun.vh | ⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 ) | |
| 7 | ushgrun.i | ⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ ) | |
| 8 | ushgrun.u | ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 ) | |
| 9 | ushgrun.v | ⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 ) | |
| 10 | ushgrun.un | ⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) ) | |
| 11 | ushgruhgr | ⊢ ( 𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph ) | |
| 12 | 1 11 | syl | ⊢ ( 𝜑 → 𝐺 ∈ UHGraph ) |
| 13 | ushgruhgr | ⊢ ( 𝐻 ∈ USHGraph → 𝐻 ∈ UHGraph ) | |
| 14 | 2 13 | syl | ⊢ ( 𝜑 → 𝐻 ∈ UHGraph ) |
| 15 | 12 14 3 4 5 6 7 8 9 10 | uhgrun | ⊢ ( 𝜑 → 𝑈 ∈ UHGraph ) |