Description: The edge function of a simple graph is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017) (Revised by AV, 15-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | usgrf1o.e | |- E = ( iEdg ` G ) |
|
| Assertion | usgrf1 | |- ( G e. USGraph -> E : dom E -1-1-> ran E ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | usgrf1o.e | |- E = ( iEdg ` G ) |
|
| 2 | 1 | usgrf1o | |- ( G e. USGraph -> E : dom E -1-1-onto-> ran E ) |
| 3 | f1of1 | |- ( E : dom E -1-1-onto-> ran E -> E : dom E -1-1-> ran E ) |
|
| 4 | 2 3 | syl | |- ( G e. USGraph -> E : dom E -1-1-> ran E ) |