Metamath Proof Explorer


Theorem usgrf1oedg

Description: The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgrf1oedg.i
|- I = ( iEdg ` G )
usgrf1oedg.e
|- E = ( Edg ` G )
Assertion usgrf1oedg
|- ( G e. USGraph -> I : dom I -1-1-onto-> E )

Proof

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 )