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

Metamath Proof Explorer

Theorem usgrausgrb

Description: The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 2-Jan-2020) (Revised by AV, 15-Oct-2020)

Ref Expression
Hypotheses ausgr.1 
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
ausgrusgri.1 
|- O = { f | f : dom f -1-1-> ran f }
Assertion usgrausgrb 
|- ( ( H e. W /\ ( iEdg ` H ) e. O ) -> ( ( Vtx ` H ) G ( Edg ` H ) <-> H e. USGraph ) )

Proof

Step Hyp Ref Expression
1 ausgr.1 
 |-  G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
2 ausgrusgri.1 
 |-  O = { f | f : dom f -1-1-> ran f }
3 1 2 ausgrusgri 
 |-  ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ ( iEdg ` H ) e. O ) -> H e. USGraph )
4 3 3exp 
 |-  ( H e. W -> ( ( Vtx ` H ) G ( Edg ` H ) -> ( ( iEdg ` H ) e. O -> H e. USGraph ) ) )
5 4 com23 
 |-  ( H e. W -> ( ( iEdg ` H ) e. O -> ( ( Vtx ` H ) G ( Edg ` H ) -> H e. USGraph ) ) )
6 5 imp 
 |-  ( ( H e. W /\ ( iEdg ` H ) e. O ) -> ( ( Vtx ` H ) G ( Edg ` H ) -> H e. USGraph ) )
7 1 usgrausgri 
 |-  ( H e. USGraph -> ( Vtx ` H ) G ( Edg ` H ) )
8 6 7 impbid1 
 |-  ( ( H e. W /\ ( iEdg ` H ) e. O ) -> ( ( Vtx ` H ) G ( Edg ` H ) <-> H e. USGraph ) )