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