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