This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uspgrf1oedg

Description: The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020) (Revised by AV, 15-Oct-2020)

Ref Expression
Hypothesis usgrf1o.e 
|- E = ( iEdg ` G )
Assertion uspgrf1oedg 
|- ( G e. USPGraph -> E : dom E -1-1-onto-> ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 usgrf1o.e 
 |-  E = ( iEdg ` G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 1 uspgrf 
 |-  ( G e. USPGraph -> E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
4 f1f1orn 
 |-  ( E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> E : dom E -1-1-onto-> ran E )
5 1 rneqi 
 |-  ran E = ran ( iEdg ` G )
6 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
7 5 6 eqtr4i 
 |-  ran E = ( Edg ` G )
8 f1oeq3 
 |-  ( ran E = ( Edg ` G ) -> ( E : dom E -1-1-onto-> ran E <-> E : dom E -1-1-onto-> ( Edg ` G ) ) )
9 7 8 ax-mp 
 |-  ( E : dom E -1-1-onto-> ran E <-> E : dom E -1-1-onto-> ( Edg ` G ) )
10 4 9 sylib 
 |-  ( E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> E : dom E -1-1-onto-> ( Edg ` G ) )
11 3 10 syl 
 |-  ( G e. USPGraph -> E : dom E -1-1-onto-> ( Edg ` G ) )