Theorem usgrausgri

Description: A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020)

	Ref	Expression
Hypothesis	ausgr.1	|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
Assertion	usgrausgri	|- ( H e. USGraph -> ( Vtx ` H ) G ( Edg ` H ) )

Proof

Step	Hyp	Ref	Expression
1		ausgr.1	|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
2		usgredgss	|- ( H e. USGraph -> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
3		fvex	|- ( Vtx ` H ) e. _V
4		fvex	|- ( Edg ` H ) e. _V
5	1	isausgr	|- ( ( ( Vtx ` H ) e. _V /\ ( Edg ` H ) e. _V ) -> ( ( Vtx ` H ) G ( Edg ` H ) <-> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
6	3 4 5	mp2an	|- ( ( Vtx ` H ) G ( Edg ` H ) <-> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
7	2 6	sylibr	|- ( H e. USGraph -> ( Vtx ` H ) G ( Edg ` H ) )