Step |
Hyp |
Ref |
Expression |
1 |
|
usgrf1oedg.i |
|- I = ( iEdg ` G ) |
2 |
|
usgrf1oedg.e |
|- E = ( Edg ` G ) |
3 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
4 |
3 1
|
usgrf |
|- ( G e. USGraph -> I : dom I -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } ) |
5 |
|
f1f1orn |
|- ( I : dom I -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> I : dom I -1-1-onto-> ran I ) |
6 |
4 5
|
syl |
|- ( G e. USGraph -> I : dom I -1-1-onto-> ran I ) |
7 |
|
edgval |
|- ( Edg ` G ) = ran ( iEdg ` G ) |
8 |
7
|
a1i |
|- ( G e. USGraph -> ( Edg ` G ) = ran ( iEdg ` G ) ) |
9 |
1
|
eqcomi |
|- ( iEdg ` G ) = I |
10 |
9
|
rneqi |
|- ran ( iEdg ` G ) = ran I |
11 |
8 10
|
eqtrdi |
|- ( G e. USGraph -> ( Edg ` G ) = ran I ) |
12 |
2 11
|
eqtrid |
|- ( G e. USGraph -> E = ran I ) |
13 |
12
|
f1oeq3d |
|- ( G e. USGraph -> ( I : dom I -1-1-onto-> E <-> I : dom I -1-1-onto-> ran I ) ) |
14 |
6 13
|
mpbird |
|- ( G e. USGraph -> I : dom I -1-1-onto-> E ) |