Description: An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 15-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | usgredgop | |- ( ( G e. USGraph /\ E = ( iEdg ` G ) /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | usgrfun | |- ( G e. USGraph -> Fun ( iEdg ` G ) ) |
|
2 | funeq | |- ( E = ( iEdg ` G ) -> ( Fun E <-> Fun ( iEdg ` G ) ) ) |
|
3 | 1 2 | syl5ibrcom | |- ( G e. USGraph -> ( E = ( iEdg ` G ) -> Fun E ) ) |
4 | 3 | imp | |- ( ( G e. USGraph /\ E = ( iEdg ` G ) ) -> Fun E ) |
5 | funopfvb | |- ( ( Fun E /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) ) |
|
6 | 4 5 | stoic3 | |- ( ( G e. USGraph /\ E = ( iEdg ` G ) /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) ) |