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 | |- ( ph -> G e. UHGraph ) |
|
| uhgrun.h | |- ( ph -> H e. UHGraph ) |
||
| uhgrun.e | |- E = ( iEdg ` G ) |
||
| uhgrun.f | |- F = ( iEdg ` H ) |
||
| uhgrun.vg | |- V = ( Vtx ` G ) |
||
| uhgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
||
| uhgrun.i | |- ( ph -> ( dom E i^i dom F ) = (/) ) |
||
| Assertion | uhgrunop | |- ( ph -> <. V , ( E u. F ) >. e. UHGraph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uhgrun.g | |- ( ph -> G e. UHGraph ) |
|
| 2 | uhgrun.h | |- ( ph -> H e. UHGraph ) |
|
| 3 | uhgrun.e | |- E = ( iEdg ` G ) |
|
| 4 | uhgrun.f | |- F = ( iEdg ` H ) |
|
| 5 | uhgrun.vg | |- V = ( Vtx ` G ) |
|
| 6 | uhgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
|
| 7 | uhgrun.i | |- ( ph -> ( dom E i^i dom F ) = (/) ) |
|
| 8 | opex | |- <. V , ( E u. F ) >. e. _V |
|
| 9 | 8 | a1i | |- ( ph -> <. V , ( E u. F ) >. e. _V ) |
| 10 | 5 | fvexi | |- V e. _V |
| 11 | 3 | fvexi | |- E e. _V |
| 12 | 4 | fvexi | |- F e. _V |
| 13 | 11 12 | unex | |- ( E u. F ) e. _V |
| 14 | 10 13 | pm3.2i | |- ( V e. _V /\ ( E u. F ) e. _V ) |
| 15 | opvtxfv | |- ( ( V e. _V /\ ( E u. F ) e. _V ) -> ( Vtx ` <. V , ( E u. F ) >. ) = V ) |
|
| 16 | 14 15 | mp1i | |- ( ph -> ( Vtx ` <. V , ( E u. F ) >. ) = V ) |
| 17 | opiedgfv | |- ( ( V e. _V /\ ( E u. F ) e. _V ) -> ( iEdg ` <. V , ( E u. F ) >. ) = ( E u. F ) ) |
|
| 18 | 14 17 | mp1i | |- ( ph -> ( iEdg ` <. V , ( E u. F ) >. ) = ( E u. F ) ) |
| 19 | 1 2 3 4 5 6 7 9 16 18 | uhgrun | |- ( ph -> <. V , ( E u. F ) >. e. UHGraph ) |