Description: The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 15-Dec-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | uhgrfun.e | |- E = ( iEdg ` G ) |
|
| Assertion | uhgrfun | |- ( G e. UHGraph -> Fun E ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uhgrfun.e | |- E = ( iEdg ` G ) |
|
| 2 | eqid | |- ( Vtx ` G ) = ( Vtx ` G ) |
|
| 3 | 2 1 | uhgrf | |- ( G e. UHGraph -> E : dom E --> ( ~P ( Vtx ` G ) \ { (/) } ) ) |
| 4 | 3 | ffund | |- ( G e. UHGraph -> Fun E ) |