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 ) |