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 | |- ( ph -> G e. USHGraph ) |
|
| ushgrun.h | |- ( ph -> H e. USHGraph ) |
||
| ushgrun.e | |- E = ( iEdg ` G ) |
||
| ushgrun.f | |- F = ( iEdg ` H ) |
||
| ushgrun.vg | |- V = ( Vtx ` G ) |
||
| ushgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
||
| ushgrun.i | |- ( ph -> ( dom E i^i dom F ) = (/) ) |
||
| ushgrun.u | |- ( ph -> U e. W ) |
||
| ushgrun.v | |- ( ph -> ( Vtx ` U ) = V ) |
||
| ushgrun.un | |- ( ph -> ( iEdg ` U ) = ( E u. F ) ) |
||
| Assertion | ushgrun | |- ( ph -> U e. UHGraph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ushgrun.g | |- ( ph -> G e. USHGraph ) |
|
| 2 | ushgrun.h | |- ( ph -> H e. USHGraph ) |
|
| 3 | ushgrun.e | |- E = ( iEdg ` G ) |
|
| 4 | ushgrun.f | |- F = ( iEdg ` H ) |
|
| 5 | ushgrun.vg | |- V = ( Vtx ` G ) |
|
| 6 | ushgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
|
| 7 | ushgrun.i | |- ( ph -> ( dom E i^i dom F ) = (/) ) |
|
| 8 | ushgrun.u | |- ( ph -> U e. W ) |
|
| 9 | ushgrun.v | |- ( ph -> ( Vtx ` U ) = V ) |
|
| 10 | ushgrun.un | |- ( ph -> ( iEdg ` U ) = ( E u. F ) ) |
|
| 11 | ushgruhgr | |- ( G e. USHGraph -> G e. UHGraph ) |
|
| 12 | 1 11 | syl | |- ( ph -> G e. UHGraph ) |
| 13 | ushgruhgr | |- ( H e. USHGraph -> H e. UHGraph ) |
|
| 14 | 2 13 | syl | |- ( ph -> H e. UHGraph ) |
| 15 | 12 14 3 4 5 6 7 8 9 10 | uhgrun | |- ( ph -> U e. UHGraph ) |