Description: The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 9-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | uhgrf.v | |- V = ( Vtx ` G ) |
|
| uhgrf.e | |- E = ( iEdg ` G ) |
||
| Assertion | uhgrf | |- ( G e. UHGraph -> E : dom E --> ( ~P V \ { (/) } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uhgrf.v | |- V = ( Vtx ` G ) |
|
| 2 | uhgrf.e | |- E = ( iEdg ` G ) |
|
| 3 | 1 2 | isuhgr | |- ( G e. UHGraph -> ( G e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) ) |
| 4 | 3 | ibi | |- ( G e. UHGraph -> E : dom E --> ( ~P V \ { (/) } ) ) |