Description: The union U of two simple pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 16-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | uspgrun.g | |- ( ph -> G e. USPGraph ) |
|
| uspgrun.h | |- ( ph -> H e. USPGraph ) |
||
| uspgrun.e | |- E = ( iEdg ` G ) |
||
| uspgrun.f | |- F = ( iEdg ` H ) |
||
| uspgrun.vg | |- V = ( Vtx ` G ) |
||
| uspgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
||
| uspgrun.i | |- ( ph -> ( dom E i^i dom F ) = (/) ) |
||
| uspgrun.u | |- ( ph -> U e. W ) |
||
| uspgrun.v | |- ( ph -> ( Vtx ` U ) = V ) |
||
| uspgrun.un | |- ( ph -> ( iEdg ` U ) = ( E u. F ) ) |
||
| Assertion | uspgrun | |- ( ph -> U e. UPGraph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uspgrun.g | |- ( ph -> G e. USPGraph ) |
|
| 2 | uspgrun.h | |- ( ph -> H e. USPGraph ) |
|
| 3 | uspgrun.e | |- E = ( iEdg ` G ) |
|
| 4 | uspgrun.f | |- F = ( iEdg ` H ) |
|
| 5 | uspgrun.vg | |- V = ( Vtx ` G ) |
|
| 6 | uspgrun.vh | |- ( ph -> ( Vtx ` H ) = V ) |
|
| 7 | uspgrun.i | |- ( ph -> ( dom E i^i dom F ) = (/) ) |
|
| 8 | uspgrun.u | |- ( ph -> U e. W ) |
|
| 9 | uspgrun.v | |- ( ph -> ( Vtx ` U ) = V ) |
|
| 10 | uspgrun.un | |- ( ph -> ( iEdg ` U ) = ( E u. F ) ) |
|
| 11 | uspgrupgr | |- ( G e. USPGraph -> G e. UPGraph ) |
|
| 12 | 1 11 | syl | |- ( ph -> G e. UPGraph ) |
| 13 | uspgrupgr | |- ( H e. USPGraph -> H e. UPGraph ) |
|
| 14 | 2 13 | syl | |- ( ph -> H e. UPGraph ) |
| 15 | 12 14 3 4 5 6 7 8 9 10 | upgrun | |- ( ph -> U e. UPGraph ) |